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

Theorem bitr4i 244
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 194 . 2  |-  ( ps  <->  ch )
41, 3bitri 241 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  3bitr2i  265  3bitr2ri  266  3bitr4i  269  3bitr4ri  270  imor  402  dfbi2  610  pm5.32  618  imdistan  671  imimorb  848  nbi2  863  pm5.6  879  mpbiran  885  mpbiran2  886  biluk  900  3anrev  947  nannan  1297  xorneg  1319  nic-ax  1444  nic-axALT  1445  19.43  1612  19.3v  1673  19.9vOLD  1706  equsalhwOLD  1857  nf3  1886  nf4  1887  equsalOLD  1967  sb6x  2078  sb5f  2089  sb3an  2119  sbequ8  2128  sb5  2149  sbhb  2156  pm11.07  2164  sbel2x  2175  eu2  2279  eu3  2280  eu5  2292  moanim  2310  2eu4  2337  2eu6  2339  cleqh  2501  cleqf  2564  necon3bii  2599  neor  2651  neorian  2654  r2alf  2701  r2exf  2702  r19.23t  2780  r19.26-3  2800  r19.26m  2801  r19.43  2823  rabid2  2845  isset  2920  ralv  2929  rexv  2930  reuv  2931  rmov  2932  rexcom4b  2937  ceqsex4v  2955  ceqsex8v  2957  ceqsrexv  3029  ralrab2  3060  rexrab2  3062  reu2  3082  reu3  3084  reueq  3091  2reuswap  3096  reuind  3097  2reu5lem3  3101  rmo2  3206  dfss2  3297  dfss3  3298  dfss3f  3300  ssabral  3374  rabss  3380  ssrabeq  3389  uniiunlem  3391  sspsstri  3409  npss  3417  uncom  3451  inass  3511  nsspssun  3534  dfss4  3535  dfun2  3536  dfin2  3537  indi  3547  indifdir  3557  difin2  3563  reupick3  3586  n0f  3596  eqv  3603  vss  3624  disj  3628  disj3  3632  undisj1  3639  undisj2  3640  inundif  3666  undif  3668  exsnrex  3808  euabsn2  3835  euabsn  3836  tppreqb  3899  pwpw0  3906  prssg  3913  ssunsn  3919  pwpr  3971  dfuni2  3977  unissb  4005  elint2  4017  ssint  4026  uniintab  4048  dfiin2g  4084  iunn0  4111  iunxun  4132  iunxiun  4133  iinpw  4139  disjor  4156  disjxiun  4169  dftr2  4264  dftr5  4265  dftr3  4266  dftr4  4267  vprc  4301  inuni  4322  snelpw  4370  sspwb  4373  pwssun  4449  dfid3  4459  dffr2  4507  dflim2  4597  orddif  4634  eusv2  4681  reusv2lem4  4686  reusv6OLD  4693  reusv7OLD  4694  rexxfr  4702  opthprc  4884  elxp3  4887  xpiundir  4892  elvv  4895  brinxp2  4898  relsn  4938  reliun  4954  inxp  4966  raliunxp  4973  cnvuni  5016  dm0rn0  5045  elrn  5069  ssdmres  5127  dfres2  5152  dfima2  5164  args  5191  dffr3  5195  cotr  5205  intasym  5208  asymref  5209  intirr  5211  cnv0  5234  xpnz  5251  xp11  5263  cnvresima  5318  resco  5333  rnco  5335  coiun  5338  coass  5347  cnvso  5370  dfiota2  5378  dffun2  5423  dffun6f  5427  dffun7  5438  dffun9  5440  funfn  5441  svrelfun  5473  dffn2  5551  dffn3  5557  fint  5581  dffn4  5618  dff1o4  5641  brprcneu  5680  eqfnfv3  5788  fnreseql  5799  fsn  5865  ftpg  5875  abrexco  5945  imaiun  5951  abexex  5962  dff13  5963  isocnv2  6010  mpt22eqb  6138  elovmpt2  6250  elxp6  6337  elxp7  6338  releldm2  6356  fnmpt2  6378  frxp  6415  dftpos4  6457  sorpss  6486  opiota  6494  tfrlem5  6600  tfrlem7  6603  ondif1  6704  oarec  6764  oeeu  6805  0er  6899  eroveu  6958  erovlem  6959  map0e  7010  elixpconst  7029  domen  7080  brsdom  7089  brdom2  7096  reuen1  7135  sbthlem10  7185  brsdom2  7190  xpf1o  7228  onfin2  7257  0sdom1dom  7265  modom  7268  unfi  7333  marypha2lem3  7400  dfsup2OLD  7406  wemapso2lem  7475  elom3  7559  dfom5  7561  trcl  7620  epfrs  7623  rankf  7676  scottexs  7767  scott0s  7768  cplem1  7769  karden  7775  hta  7777  pm54.43lem  7842  alephsuc2  7917  iscard3  7930  aceq0  7955  aceq3lem  7957  dfac3  7958  dfac5lem2  7961  dfac5  7965  dfac7  7968  dfac12a  7984  kmlem12  7997  kmlem14  7999  kmlem15  8000  infmap2  8054  ackbij2  8079  dfacfin7  8235  ituniiun  8258  zorng  8340  brdom7disj  8365  entri2  8389  alephreg  8413  fpwwe2lem12  8472  fpwwe2lem13  8473  pwfseqlem1  8489  grutsk  8653  axgroth4  8663  grothprim  8665  grothtsk  8666  elni2  8710  ltsopi  8721  genpass  8842  psslinpr  8864  ltexprlem4  8872  ltresr  8971  1re  9046  infm3  9923  elnnz  10248  dfz2  10255  2rexuz  10485  nnwos  10500  eluz2b1  10503  qexALT  10545  elxr  10672  dflt2  10697  xrsupss  10843  xrinfmss  10844  elixx1  10881  elioo2  10913  elioopnf  10954  elicopnf  10956  elfz1  11004  fznn0  11069  fznn  11070  injresinj  11155  nn0opthlem1  11516  faclbnd4lem1  11539  hashf  11580  hashfun  11655  hashf1  11661  fz1isolem  11665  f1oun2prg  11819  shftdm  11841  rediv  11891  imdiv  11898  rexanre  12105  caubnd  12117  climreu  12305  dvdslelem  12849  bitsval  12891  smueqlem  12957  algcvgblem  13023  isprm2  13042  isprm3  13043  isprm4  13044  pythagtriplem2  13146  elgz  13254  hashbc0  13328  0ram  13343  isstruct  13434  issect  13934  isfull2  14063  isfth2  14067  fucinv  14125  eldmcoa  14175  isdrs  14346  fpwipodrs  14545  submacs  14720  isnsg4  14938  isgim  15004  gaorb  15039  oppgid  15107  oppgsubm  15113  oppgcntz  15115  ispgp  15181  efgsdm  15317  efgcpbllema  15341  iscyg2  15447  isrng  15623  isirred2  15761  opprirred  15762  dfrhm2  15776  drngid2  15806  opprsubrg  15844  islmod  15909  lss1d  15994  islmhm  16058  islmim  16089  lbsextlem2  16186  lidlnz  16254  lidldvgen  16281  isnzr2  16289  isassa  16330  dfprm2  16729  isphl  16814  elocv  16850  iunocv  16863  isobs  16902  isbasis3g  16969  fctop  17023  cctop  17025  isclo2  17107  restsn  17188  lmbr  17276  ist0-3  17363  2ndcdisj  17472  1stccnp  17478  1stckgenlem  17538  txbas  17552  ptbasin  17562  tx2cn  17595  fbfinnfr  17826  fbasrn  17869  filuni  17870  ufinffr  17914  fin1aufil  17917  rnelfmlem  17937  flimrest  17968  alexsubALTlem3  18033  alexsubALTlem4  18034  tgphaus  18099  istlm  18167  iscusp2  18285  metuel2  18562  isngp2  18597  isnlm  18664  elcncf1di  18878  isphtpc  18972  phtpcer  18973  om1elbas  19010  isclm  19042  iscph  19086  iscau3  19184  minveclem3b  19282  elovolm  19324  ioombl1lem4  19408  dyaddisj  19441  vitali  19458  itg1climres  19559  itg2seq  19587  itg2monolem1  19595  itg2mono  19598  limcrcl  19714  lhop1  19851  itgsubst  19886  isuc1p  20016  ismon1p  20018  plydivex  20167  ellogdm  20483  1cubr  20635  atandm2  20670  birthdaylem3  20745  dmarea  20749  dchrelbas2  20974  dchrelbas4  20980  nb3grapr  21415  nb3grapr2  21416  cusgrarn  21421  usgrasscusgra  21445  3v3e3cycl2  21604  isgrpo2  21738  nmoubi  22226  nmobndseqi  22233  nmobndseqiOLD  22234  minvecolem1  22329  isch2  22679  hlimreui  22695  isch3  22697  ocsh  22738  dfch2  22862  spanuni  22999  nonbooli  23106  5oalem7  23115  adjsym  23289  elbdop2  23327  dmadjss  23343  nmopub  23364  nmfnleub  23381  nmop0h  23447  pjssposi  23628  pjordi  23629  cvbr2  23739  cvnbtwn2  23743  mdsl2i  23778  cvmdi  23780  elat2  23796  atom1d  23809  chirredi  23850  cdj3i  23897  or3di  23904  rabid2f  23920  mo5f  23925  2reuswap2  23928  rexunirn  23931  iuneq12daf  23960  iuneq12df  23961  iuninc  23964  disjorf  23974  rabfmpunirn  24018  mptfnf  24026  funcnv5mpt  24037  eliccelico  24093  elicoelioo  24094  isofld  24188  hasheuni  24428  pwsiga  24466  sigainb  24472  2ndmbfm  24564  probun  24630  ballotlem2  24699  ballotlemodife  24708  erdszelem9  24838  erdszelem10  24839  pconcon  24871  cvmliftiota  24941  nepss  25128  fzp1nel  25163  prodmo  25215  dfso2  25325  dfpo2  25326  dfres3  25330  elrn3  25334  elpotr  25351  dfon2lem3  25355  dfon2lem5  25357  dfon2lem7  25359  dfon2lem8  25360  predreseq  25393  cbvsetlike  25395  dffr4  25396  preduz  25414  wfi  25421  frind  25457  soseq  25468  wfrlem5  25474  wfrlem8  25477  wfrlem11  25480  frrlem5  25499  frrlem5c  25501  elno3  25523  nosgnn0  25526  nocvxminlem  25558  nofulllem5  25574  symdifass  25585  brtxp2  25635  brpprod3a  25640  eltrans  25645  dfon3  25646  elfuns  25668  brsingle  25670  brsuccf  25694  funpartfun  25696  funpartfv  25698  axcontlem7  25813  cgrxfr  25893  segletr  25952  outsideoftr  25967  df3nandALT1  26050  rabiun2  26139  ismblfin  26146  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  itg2addnclem2  26156  islocfin  26266  neifg  26290  filnetlem4  26300  fdc  26339  nninfnub  26345  prdstotbnd  26393  isdrngo1  26462  ispridl  26534  ismaxidl  26540  prter1  26618  raldifsni  26624  rexrabdioph  26744  dford4  26990  islinds  27147  issdrg  27373  isdomn3  27391  pm11.52  27453  pm11.58  27457  pm13.192  27478  conss34  27512  bothtbothsame  27734  bothfbothsame  27735  aiffbtbat  27743  rmoanim  27824  2rmoswap  27829  frgra3v  28106  2spotdisj  28164  impexp3acom3r  28309  opelopab4  28349  uunT12p1  28621  uunT12p2  28622  uunT12p3  28623  uun2221  28634  uun2221p1  28635  uun2221p2  28636  undif3VD  28703  onfrALTlem5VD  28706  bnj252  28773  bnj253  28774  bnj255  28775  bnj345  28784  bnj133  28798  bnj976  28854  bnj1098  28860  bnj121  28947  bnj130  28951  bnj150  28953  bnj581  28985  bnj607  28993  bnj865  29000  bnj917  29011  bnj934  29012  bnj964  29020  bnj983  29028  bnj996  29032  bnj1021  29041  bnj1033  29044  bnj1047  29048  bnj1049  29049  bnj1090  29054  bnj1128  29065  bnj1175  29079  bnj1189  29084  bnj1204  29087  bnj1253  29092  bnj1312  29133  equsalNEW7  29193  sbequ8NEW7  29279  sb5NEW7  29299  sbhbwAUX7  29308  sbel2xNEW7  29315  sb6xNEW7  29330  sb5fNEW7  29335  sb3anNEW7  29341  sbhbOLD7  29444  islshp  29462  islshpat  29500  lcvbr2  29505  lcvnbtwn2  29510  cvrnbtwn3  29759  isatl  29782  ishlat1  29835  ishlat2  29836  cvrat4  29925  pmapglbx  30251  lhpexle3  30494  dib1dim  31648  diblsmopel  31654  lcfls1lem  32017
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 178
  Copyright terms: Public domain W3C validator