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  1672  19.9vOLD  1704  equsalhwOLD  1851  nf3  1879  nf4  1880  equsalOLD  1955  sb6x  2062  sb5f  2073  sb3an  2103  sbequ8  2112  sb5  2133  sbhb  2140  pm11.07  2148  sbel2x  2159  eu2  2263  eu3  2264  eu5  2276  moanim  2294  2eu4  2321  2eu6  2323  cleqh  2484  cleqf  2547  necon3bii  2582  neor  2634  neorian  2637  r2alf  2684  r2exf  2685  r19.23t  2763  r19.26-3  2783  r19.26m  2784  r19.43  2806  rabid2  2828  isset  2903  ralv  2912  rexv  2913  reuv  2914  rmov  2915  rexcom4b  2920  ceqsex4v  2938  ceqsex8v  2940  ceqsrexv  3012  ralrab2  3043  rexrab2  3045  reu2  3065  reu3  3067  reueq  3074  2reuswap  3079  reuind  3080  2reu5lem3  3084  rmo2  3189  dfss2  3280  dfss3  3281  dfss3f  3283  ssabral  3357  rabss  3363  ssrabeq  3372  uniiunlem  3374  sspsstri  3392  npss  3400  uncom  3434  inass  3494  nsspssun  3517  dfss4  3518  dfun2  3519  dfin2  3520  indi  3530  indifdir  3540  difin2  3546  reupick3  3569  n0f  3579  eqv  3586  vss  3607  disj  3611  disj3  3615  undisj1  3622  undisj2  3623  inundif  3649  undif  3651  exsnrex  3791  euabsn2  3818  euabsn  3819  tppreqb  3882  pwpw0  3889  prssg  3896  ssunsn  3902  pwpr  3953  dfuni2  3959  unissb  3987  elint2  3999  ssint  4008  uniintab  4030  dfiin2g  4066  iunn0  4092  iunxun  4113  iunxiun  4114  iinpw  4120  disjor  4137  disjxiun  4150  dftr2  4245  dftr5  4246  dftr3  4247  dftr4  4248  vprc  4282  inuni  4303  snelpw  4351  sspwb  4354  pwssun  4430  dfid3  4440  dffr2  4488  dflim2  4578  orddif  4615  eusv2  4662  reusv2lem4  4667  reusv6OLD  4674  reusv7OLD  4675  rexxfr  4683  opthprc  4865  elxp3  4868  xpiundir  4873  elvv  4876  brinxp2  4879  relsn  4919  reliun  4935  inxp  4947  raliunxp  4954  cnvuni  4997  dm0rn0  5026  elrn  5050  ssdmres  5108  dfres2  5133  dfima2  5145  args  5172  dffr3  5176  cotr  5186  intasym  5189  asymref  5190  intirr  5192  cnv0  5215  xpnz  5232  xp11  5244  cnvresima  5299  resco  5314  rnco  5316  coiun  5319  coass  5328  cnvso  5351  dfiota2  5359  dffun2  5404  dffun6f  5408  dffun7  5419  dffun9  5421  funfn  5422  svrelfun  5454  dffn2  5532  dffn3  5538  fint  5562  dffn4  5599  dff1o4  5622  brprcneu  5661  eqfnfv3  5768  fnreseql  5779  fsn  5845  ftpg  5855  abrexco  5925  imaiun  5931  abexex  5942  dff13  5943  isocnv2  5990  mpt22eqb  6118  elovmpt2  6230  elxp6  6317  elxp7  6318  releldm2  6336  fnmpt2  6358  frxp  6392  dftpos4  6434  sorpss  6463  opiota  6471  tfrlem5  6577  tfrlem7  6580  ondif1  6681  oarec  6741  oeeu  6782  0er  6876  eroveu  6935  erovlem  6936  map0e  6987  elixpconst  7006  domen  7057  brsdom  7066  brdom2  7073  reuen1  7112  sbthlem10  7162  brsdom2  7167  xpf1o  7205  onfin2  7234  0sdom1dom  7242  modom  7245  unfi  7310  marypha2lem3  7377  dfsup2OLD  7383  wemapso2lem  7452  elom3  7536  dfom5  7538  trcl  7597  epfrs  7600  rankf  7653  scottexs  7744  scott0s  7745  cplem1  7746  karden  7752  hta  7754  pm54.43lem  7819  alephsuc2  7894  iscard3  7907  aceq0  7932  aceq3lem  7934  dfac3  7935  dfac5lem2  7938  dfac5  7942  dfac7  7945  dfac12a  7961  kmlem12  7974  kmlem14  7976  kmlem15  7977  infmap2  8031  ackbij2  8056  dfacfin7  8212  ituniiun  8235  zorng  8317  brdom7disj  8342  entri2  8366  alephreg  8390  fpwwe2lem12  8449  fpwwe2lem13  8450  pwfseqlem1  8466  grutsk  8630  axgroth4  8640  grothprim  8642  grothtsk  8643  elni2  8687  ltsopi  8698  genpass  8819  psslinpr  8841  ltexprlem4  8849  ltresr  8948  1re  9023  infm3  9899  elnnz  10224  dfz2  10231  2rexuz  10461  nnwos  10476  eluz2b1  10479  qexALT  10521  elxr  10648  dflt2  10673  xrsupss  10819  xrinfmss  10820  elixx1  10857  elioo2  10889  elioopnf  10930  elicopnf  10932  elfz1  10980  fznn0  11044  fznn  11045  injresinj  11127  nn0opthlem1  11488  faclbnd4lem1  11511  hashf  11552  hashfun  11627  hashf1  11633  fz1isolem  11637  f1oun2prg  11791  shftdm  11813  rediv  11863  imdiv  11870  rexanre  12077  caubnd  12089  climreu  12277  dvdslelem  12821  bitsval  12863  smueqlem  12929  algcvgblem  12995  isprm2  13014  isprm3  13015  isprm4  13016  pythagtriplem2  13118  elgz  13226  hashbc0  13300  0ram  13315  isstruct  13406  issect  13906  isfull2  14035  isfth2  14039  fucinv  14097  eldmcoa  14147  isdrs  14318  fpwipodrs  14517  submacs  14692  isnsg4  14910  isgim  14976  gaorb  15011  oppgid  15079  oppgsubm  15085  oppgcntz  15087  ispgp  15153  efgsdm  15289  efgcpbllema  15313  iscyg2  15419  isrng  15595  isirred2  15733  opprirred  15734  dfrhm2  15748  drngid2  15778  opprsubrg  15816  islmod  15881  lss1d  15966  islmhm  16030  islmim  16061  lbsextlem2  16158  lidlnz  16226  lidldvgen  16253  isnzr2  16261  isassa  16302  dfprm2  16697  isphl  16782  elocv  16818  iunocv  16831  isobs  16870  isbasis3g  16937  fctop  16991  cctop  16993  isclo2  17075  restsn  17156  lmbr  17244  ist0-3  17331  2ndcdisj  17440  1stccnp  17446  1stckgenlem  17506  txbas  17520  ptbasin  17530  tx2cn  17563  fbfinnfr  17794  fbasrn  17837  filuni  17838  ufinffr  17882  fin1aufil  17885  rnelfmlem  17905  flimrest  17936  alexsubALTlem3  18001  alexsubALTlem4  18002  tgphaus  18067  istlm  18135  iscusp2  18253  metuel2  18485  isngp2  18515  isnlm  18582  elcncf1di  18796  isphtpc  18890  phtpcer  18891  om1elbas  18928  isclm  18960  iscph  19004  iscau3  19102  minveclem3b  19196  elovolm  19238  ioombl1lem4  19322  dyaddisj  19355  vitali  19372  itg1climres  19473  itg2seq  19501  itg2monolem1  19509  itg2mono  19512  limcrcl  19628  lhop1  19765  itgsubst  19800  isuc1p  19930  ismon1p  19932  plydivex  20081  ellogdm  20397  1cubr  20549  atandm2  20584  birthdaylem3  20659  dmarea  20663  dchrelbas2  20888  dchrelbas4  20894  nb3grapr  21328  nb3grapr2  21329  cusgrarn  21334  usgrasscusgra  21358  3v3e3cycl2  21499  isgrpo2  21633  nmoubi  22121  nmobndseqi  22128  nmobndseqiOLD  22129  minvecolem1  22224  isch2  22574  hlimreui  22590  isch3  22592  ocsh  22633  dfch2  22757  spanuni  22894  nonbooli  23001  5oalem7  23010  adjsym  23184  elbdop2  23222  dmadjss  23238  nmopub  23259  nmfnleub  23276  nmop0h  23342  pjssposi  23523  pjordi  23524  cvbr2  23634  cvnbtwn2  23638  mdsl2i  23673  cvmdi  23675  elat2  23691  atom1d  23704  chirredi  23745  cdj3i  23792  or3di  23799  rabid2f  23811  mo5f  23816  2reuswap2  23819  rexunirn  23822  iuneq12daf  23851  iuneq12df  23852  iuninc  23855  disjorf  23865  rabfmpunirn  23907  mptfnf  23915  funcnv5mpt  23925  eliccelico  23976  elicoelioo  23977  isofld  24061  hasheuni  24271  pwsiga  24309  sigainb  24315  2ndmbfm  24405  probun  24456  ballotlem2  24525  ballotlemodife  24534  erdszelem9  24664  erdszelem10  24665  pconcon  24697  cvmliftiota  24767  nepss  24954  fzp1nel  24989  prodmo  25041  dfso2  25135  dfpo2  25136  dfres3  25140  elrn3  25144  elpotr  25161  dfon2lem3  25165  dfon2lem5  25167  dfon2lem7  25169  dfon2lem8  25170  predreseq  25203  cbvsetlike  25205  dffr4  25206  preduz  25224  wfi  25231  frind  25267  soseq  25278  wfrlem5  25284  wfrlem8  25287  wfrlem11  25290  frrlem5  25309  frrlem5c  25311  elno3  25333  nosgnn0  25336  nocvxminlem  25368  nofulllem5  25384  symdifass  25395  brtxp2  25445  brpprod3a  25450  eltrans  25455  dfon3  25456  elfuns  25478  brsingle  25480  brsuccf  25504  funpartfun  25506  funpartfv  25508  axcontlem7  25623  cgrxfr  25703  segletr  25762  outsideoftr  25777  df3nandALT1  25860  rabiun2  25949  ovoliunnfl  25953  voliunnfl  25955  volsupnfl  25956  itg2addnclem2  25958  itg2addnc  25959  itgaddnclem2  25964  islocfin  26067  neifg  26091  filnetlem4  26101  fdc  26140  nninfnub  26146  prdstotbnd  26194  isdrngo1  26263  ispridl  26335  ismaxidl  26341  prter1  26419  raldifsni  26425  rexrabdioph  26545  dford4  26791  islinds  26948  issdrg  27174  isdomn3  27192  pm11.52  27254  pm11.58  27258  pm13.192  27279  conss34  27313  bothtbothsame  27535  bothfbothsame  27536  aiffbtbat  27544  rmoanim  27625  2rmoswap  27630  frgra3v  27755  impexp3acom3r  27941  opelopab4  27981  uunT12p1  28253  uunT12p2  28254  uunT12p3  28255  uun2221  28266  uun2221p1  28267  uun2221p2  28268  undif3VD  28335  onfrALTlem5VD  28338  bnj252  28405  bnj253  28406  bnj255  28407  bnj345  28416  bnj133  28430  bnj976  28486  bnj1098  28492  bnj121  28579  bnj130  28583  bnj150  28585  bnj581  28617  bnj607  28625  bnj865  28632  bnj917  28643  bnj934  28644  bnj964  28652  bnj983  28660  bnj996  28664  bnj1021  28673  bnj1033  28676  bnj1047  28680  bnj1049  28681  bnj1090  28686  bnj1128  28697  bnj1175  28711  bnj1189  28716  bnj1204  28719  bnj1253  28724  bnj1312  28765  equsalNEW7  28825  sbequ8NEW7  28911  sb5NEW7  28931  sbhbwAUX7  28940  sbel2xNEW7  28947  sb6xNEW7  28962  sb5fNEW7  28967  sb3anNEW7  28973  sbhbOLD7  29076  islshp  29094  islshpat  29132  lcvbr2  29137  lcvnbtwn2  29142  cvrnbtwn3  29391  isatl  29414  ishlat1  29467  ishlat2  29468  cvrat4  29557  pmapglbx  29883  lhpexle3  30126  dib1dim  31280  diblsmopel  31286  lcfls1lem  31649
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