MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitr4i Unicode version

Theorem bitr4i 243
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr4i.1  |-  ( ph  <->  ps )
bitr4i.2  |-  ( ch  <->  ps )
Assertion
Ref Expression
bitr4i  |-  ( ph  <->  ch )

Proof of Theorem bitr4i
StepHypRef Expression
1 bitr4i.1 . 2  |-  ( ph  <->  ps )
2 bitr4i.2 . . 3  |-  ( ch  <->  ps )
32bicomi 193 . 2  |-  ( ps  <->  ch )
41, 3bitri 240 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  3bitr2i  264  3bitr2ri  265  3bitr4i  268  3bitr4ri  269  imor  401  dfbi2  609  pm5.32  617  imdistan  670  imimorb  847  nbi2  862  pm5.6  878  mpbiran  884  mpbiran2  885  biluk  899  3anrev  945  nannan  1291  xorneg  1304  nic-ax  1428  nic-axALT  1429  19.43  1595  19.3v  1654  19.9vOLD  1682  equsalhw  1742  nf3  1811  nf4  1812  equsal  1913  sb6x  1982  sb5f  1993  sb3an  2023  sbequ8  2032  sb5  2052  sbhb  2059  sbel2x  2077  eu2  2181  eu3  2182  eu5  2194  moanim  2212  2eu4  2239  2eu6  2241  cleqh  2393  cleqf  2456  necon3bii  2491  neor  2543  neorian  2546  r2alf  2591  r2exf  2592  r19.23t  2670  r19.26-3  2690  r19.26m  2691  r19.43  2708  rabid2  2730  isset  2805  ralv  2814  rexv  2815  reuv  2816  rmov  2817  rexcom4b  2822  ceqsex4v  2840  ceqsex8v  2842  ceqsrexv  2914  ralrab2  2944  rexrab2  2946  reu2  2966  reu3  2968  reueq  2975  2reuswap  2980  reuind  2981  2reu5lem3  2985  rmo2  3089  dfss2  3182  dfss3  3183  dfss3f  3185  ssabral  3257  rabss  3263  uniiunlem  3273  sspsstri  3291  npss  3299  uncom  3332  inass  3392  nsspssun  3415  dfss4  3416  dfun2  3417  dfin2  3418  indi  3428  indifdir  3438  difin2  3443  reupick3  3466  n0f  3476  eqv  3483  vss  3504  disj  3508  disj3  3512  undisj1  3519  undisj2  3520  inundif  3545  undif  3547  euabsn2  3711  euabsn  3712  pwpw0  3779  prssg  3786  ssunsn  3790  pwpr  3839  dfuni2  3845  unissb  3873  elint2  3885  ssint  3894  uniintab  3916  dfiin2g  3952  iunn0  3978  iunxun  3999  iunxiun  4000  iinpw  4006  disjor  4023  disjxiun  4036  dftr2  4131  dftr5  4132  dftr3  4133  dftr4  4134  vprc  4168  inuni  4189  snelpw  4237  sspwb  4239  pwssun  4315  dfid3  4326  dffr2  4374  dflim2  4464  orddif  4502  eusv2  4549  reusv2lem4  4554  reusv6OLD  4561  reusv7OLD  4562  rexxfr  4570  opthprc  4752  elxp3  4755  xpiundir  4760  elvv  4764  brinxp2  4767  relsn  4806  reliun  4822  inxp  4834  raliunxp  4841  cnvuni  4882  dm0rn0  4911  elrn  4935  ssdmres  4993  dfres2  5018  dfima2  5030  args  5057  dffr3  5061  cotr  5071  intasym  5074  asymref  5075  intirr  5077  cnv0  5100  xpnz  5115  xp11  5127  cnvresima  5178  resco  5193  rnco  5195  coiun  5198  coass  5207  cnvso  5230  dfiota2  5236  dffun2  5281  dffun6f  5285  dffun7  5296  dffun9  5298  funfn  5299  svrelfun  5329  dffn2  5406  dffn3  5412  fint  5436  dffn4  5473  dff1o4  5496  brprcneu  5534  eqfnfv3  5640  fnreseql  5651  fsn  5712  abrexco  5782  imaiun  5787  abexex  5798  dff13  5799  isocnv2  5844  mpt22eqb  5969  elovmpt2  6080  elxp6  6167  elxp7  6168  releldm2  6186  fnmpt2  6208  frxp  6241  dftpos4  6269  sorpss  6298  opiota  6306  tfrlem5  6412  tfrlem7  6415  ondif1  6516  oarec  6576  oeeu  6617  0er  6711  eroveu  6769  erovlem  6770  map0e  6821  elixpconst  6840  domen  6891  brsdom  6900  brdom2  6907  reuen1  6946  sbthlem10  6996  brsdom2  7001  xpf1o  7039  onfin2  7068  0sdom1dom  7076  modom  7079  unfi  7140  marypha2lem3  7206  dfsup2OLD  7212  wemapso2lem  7281  elom3  7365  dfom5  7367  trcl  7426  epfrs  7429  rankf  7482  scottexs  7573  scott0s  7574  cplem1  7575  karden  7581  hta  7583  pm54.43lem  7648  alephsuc2  7723  iscard3  7736  aceq0  7761  aceq3lem  7763  dfac3  7764  dfac5lem2  7767  dfac5  7771  dfac7  7774  dfac12a  7790  kmlem12  7803  kmlem14  7805  kmlem15  7806  infmap2  7860  ackbij2  7885  ominf4  7954  dfacfin7  8041  ituniiun  8064  zorng  8147  brdom7disj  8172  entri2  8196  alephreg  8220  fpwwe2lem12  8279  fpwwe2lem13  8280  pwfseqlem1  8296  grutsk  8460  axgroth4  8470  grothprim  8472  grothtsk  8473  elni2  8517  ltsopi  8528  genpass  8649  psslinpr  8671  ltexprlem4  8679  ltresr  8778  1re  8853  infm3  9729  elnnz  10050  dfz2  10057  2rexuz  10287  nnwos  10302  eluz2b1  10305  qexALT  10347  elxr  10474  dflt2  10498  xrsupss  10643  xrinfmss  10644  elixx1  10681  elioo2  10713  elioopnf  10753  elicopnf  10755  elfz1  10803  fznn0  10867  fznn  10868  nn0opthlem1  11299  faclbnd4lem1  11322  hashf  11360  hashfun  11405  hashf1  11411  fz1isolem  11415  shftdm  11582  rediv  11632  imdiv  11639  rexanre  11846  caubnd  11858  climreu  12046  dvdslelem  12589  bitsval  12631  smueqlem  12697  algcvgblem  12763  isprm2  12782  isprm3  12783  isprm4  12784  pythagtriplem2  12886  elgz  12994  hashbc0  13068  0ram  13083  isstruct  13174  issect  13672  isssc  13713  isfull2  13801  isfth2  13805  fucinv  13863  eldmcoa  13913  isdrs  14084  fpwipodrs  14283  submacs  14458  isnsg4  14676  isgim  14742  gaorb  14777  oppgid  14845  oppgsubm  14851  oppgcntz  14853  ispgp  14919  efgsdm  15055  efgcpbllema  15079  iscyg2  15185  isrng  15361  isirred2  15499  opprirred  15500  dfrhm2  15514  drngid2  15544  opprsubrg  15582  islmod  15647  lss1d  15736  islmhm  15800  islmim  15831  lbsextlem2  15928  lidlnz  15996  lidldvgen  16023  isnzr2  16031  isassa  16072  dfprm2  16463  isphl  16548  elocv  16584  iunocv  16597  isobs  16636  isbasis3g  16703  fctop  16757  cctop  16759  isclo2  16841  restsn  16917  lmbr  17004  ist0-3  17089  2ndcdisj  17198  1stccnp  17204  1stckgenlem  17264  txbas  17278  ptbasin  17288  tx2cn  17320  fbfinnfr  17552  fbasrn  17595  filuni  17596  ufinffr  17640  fin1aufil  17643  rnelfmlem  17663  flimrest  17694  alexsubALTlem3  17759  alexsubALTlem4  17760  tgphaus  17815  istlm  17883  isngp2  18135  isnlm  18202  elcncf1di  18415  isphtpc  18508  phtpcer  18509  om1elbas  18546  isclm  18578  iscph  18622  iscau3  18720  minveclem3b  18808  elovolm  18850  ioombl1lem4  18934  dyaddisj  18967  vitali  18984  itg1climres  19085  itg2seq  19113  itg2monolem1  19121  itg2mono  19124  limcrcl  19240  lhop1  19377  itgsubst  19412  isuc1p  19542  ismon1p  19544  plydivex  19693  ellogdm  20002  1cubr  20154  atandm2  20189  birthdaylem3  20264  dmarea  20268  dchrelbas2  20492  dchrelbas4  20498  isgrpo2  20880  nmoubi  21366  nmobndseqi  21373  nmobndseqiOLD  21374  minvecolem1  21469  isch2  21819  hlimreui  21835  isch3  21837  ocsh  21878  dfch2  22002  spanuni  22139  nonbooli  22246  5oalem7  22255  adjsym  22429  elbdop2  22467  dmadjss  22483  nmopub  22504  nmfnleub  22521  nmop0h  22587  pjssposi  22768  pjordi  22769  cvbr2  22879  cvnbtwn2  22883  mdsl2i  22918  cvmdi  22920  elat2  22936  atom1d  22949  chirredi  22990  cdj3i  23037  ballotlem2  23063  ballotlemodife  23072  or3di  23139  rabid2f  23151  2reuswap2  23153  rexunirn  23156  mo5f  23159  iuneq12daf  23170  iuneq12df  23171  iuninc  23174  disjex  23192  disjexc  23193  rabfmpunirn  23232  mptfnf  23241  funcnv5mpt  23251  eliccelico  23285  elicoelioo  23286  disjorf  23371  hasheuni  23468  pwsiga  23506  sigainb  23512  2ndmbfm  23581  isibfm  23608  probun  23637  erdszelem9  23745  erdszelem10  23746  pconcon  23777  cvmliftiota  23847  nepss  24087  prodmo  24159  dfso2  24181  dfpo2  24182  dfres3  24186  elrn3  24190  elpotr  24207  dfon2lem3  24211  dfon2lem5  24213  dfon2lem7  24215  dfon2lem8  24216  predreseq  24249  cbvsetlike  24251  dffr4  24252  preduz  24270  wfi  24277  frind  24313  soseq  24324  wfrlem5  24330  wfrlem8  24333  wfrlem11  24336  frrlem5  24355  frrlem5c  24357  elno3  24379  nosgnn0  24382  nocvxminlem  24414  nofulllem5  24430  symdifass  24441  brtxp2  24491  brpprod3a  24496  eltrans  24501  dfon3  24502  elfuns  24524  brsingle  24526  brsuccf  24550  funpartfun  24552  funpartfv  24554  axcontlem7  24669  cgrxfr  24749  segletr  24808  outsideoftr  24823  df3nandALT1  24906  rabiun2  24996  ovoliunnfl  25000  itg2addnclem2  25003  itg2addnc  25004  itgaddnclem2  25009  dfdir2  25393  ishomc  25891  isconcl7a  26207  isibcg  26293  cnvresimaOLD  26328  islocfin  26398  neifg  26422  filnetlem4  26432  fdc  26557  nninfnub  26563  prdstotbnd  26620  isdrngo1  26689  ispridl  26761  ismaxidl  26767  prter1  26849  raldifsni  26855  rexrabdioph  26977  dford4  27224  islinds  27381  issdrg  27607  isdomn3  27625  pm11.52  27687  pm11.58  27691  pm13.192  27712  conss34  27747  stoweidlem52  27903  rmoanim  28059  2rmoswap  28064  f1oun2prg  28186  mpt2xopynvov0g  28195  injresinj  28214  nb3grapr  28288  nb3grapr2  28289  3v3e3cycl2  28409  frgra3v  28425  impexp3acom3r  28575  opelopab4  28615  uunT12p1  28888  uunT12p2  28889  uunT12p3  28890  uun2221  28901  uun2221p1  28902  uun2221p2  28903  undif3VD  28973  onfrALTlem5VD  28976  bnj252  29043  bnj253  29044  bnj255  29045  bnj345  29054  bnj133  29068  bnj976  29124  bnj1098  29130  bnj121  29217  bnj130  29221  bnj150  29223  bnj581  29255  bnj607  29263  bnj865  29270  bnj917  29281  bnj934  29282  bnj964  29290  bnj983  29298  bnj996  29302  bnj1021  29311  bnj1033  29314  bnj1047  29318  bnj1049  29319  bnj1090  29324  bnj1128  29335  bnj1175  29349  bnj1189  29354  bnj1204  29357  bnj1253  29362  bnj1312  29403  equsalNEW7  29463  sbequ8NEW7  29549  sb5NEW7  29569  sbhbwAUX7  29578  sbel2xNEW7  29585  sb6xNEW7  29600  sb5fNEW7  29605  sb3anNEW7  29611  sbhbOLD7  29714  anandii  29729  islshp  29791  islshpat  29829  lcvbr2  29834  lcvnbtwn2  29839  cvrnbtwn3  30088  isatl  30111  ishlat1  30164  ishlat2  30165  cvrat4  30254  pmapglbx  30580  lhpexle3  30823  dib1dim  31977  diblsmopel  31983  lcfls1lem  32346
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator