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  1592  19.9v  1663  equsalhw  1730  nf3  1799  nf4  1800  equsal  1900  sb6x  1969  sb5f  1980  sb3an  2010  sbequ8  2019  sb5  2039  sbhb  2046  sbel2x  2064  eu2  2168  eu3  2169  eu5  2181  moanim  2199  2eu4  2226  2eu6  2228  cleqh  2380  cleqf  2443  necon3bii  2478  neor  2530  neorian  2533  r2alf  2578  r2exf  2579  r19.23t  2657  r19.26-3  2677  r19.26m  2678  r19.43  2695  rabid2  2717  isset  2792  ralv  2801  rexv  2802  reuv  2803  rmov  2804  rexcom4b  2809  ceqsex4v  2827  ceqsex8v  2829  ceqsrexv  2901  ralrab2  2931  rexrab2  2933  reu2  2953  reu3  2955  reueq  2962  2reuswap  2967  reuind  2968  2reu5lem3  2972  rmo2  3076  dfss2  3169  dfss3  3170  dfss3f  3172  ssabral  3244  rabss  3250  uniiunlem  3260  sspsstri  3278  npss  3286  uncom  3319  inass  3379  nsspssun  3402  dfss4  3403  dfun2  3404  dfin2  3405  indi  3415  indifdir  3425  difin2  3430  reupick3  3453  n0f  3463  eqv  3470  vss  3491  disj  3495  disj3  3499  undisj1  3506  undisj2  3507  inundif  3532  undif  3534  euabsn2  3698  euabsn  3699  pwpw0  3763  prssg  3770  ssunsn  3774  pwpr  3823  dfuni2  3829  unissb  3857  elint2  3869  ssint  3878  uniintab  3900  dfiin2g  3936  iunn0  3962  iunxun  3983  iunxiun  3984  iinpw  3990  disjor  4007  disjxiun  4020  dftr2  4115  dftr5  4116  dftr3  4117  dftr4  4118  vprc  4152  inuni  4173  snelpw  4221  sspwb  4223  pwssun  4299  dfid3  4310  dffr2  4358  dflim2  4448  orddif  4486  eusv2  4533  reusv2lem4  4538  reusv6OLD  4545  reusv7OLD  4546  rexxfr  4554  opthprc  4736  elxp3  4739  xpiundir  4744  elvv  4748  brinxp2  4751  relsn  4790  reliun  4806  inxp  4818  raliunxp  4825  cnvuni  4866  dm0rn0  4895  elrn  4919  ssdmres  4977  dfres2  5002  dfima2  5014  args  5041  dffr3  5045  cotr  5055  intasym  5058  asymref  5059  intirr  5061  cnv0  5084  xpnz  5099  xp11  5111  cnvresima  5162  resco  5177  rnco  5179  coiun  5182  coass  5191  cnvso  5214  dfiota2  5220  dffun2  5265  dffun6f  5269  dffun7  5280  dffun9  5282  funfn  5283  svrelfun  5313  dffn2  5390  dffn3  5396  fint  5420  dffn4  5457  dff1o4  5480  brprcneu  5518  eqfnfv3  5624  fnreseql  5635  fsn  5696  abrexco  5766  imaiun  5771  abexex  5782  dff13  5783  isocnv2  5828  mpt22eqb  5953  elovmpt2  6064  elxp6  6151  elxp7  6152  releldm2  6170  fnmpt2  6192  frxp  6225  dftpos4  6253  sorpss  6282  opiota  6290  tfrlem5  6396  tfrlem7  6399  ondif1  6500  oarec  6560  oeeu  6601  0er  6695  eroveu  6753  erovlem  6754  map0e  6805  elixpconst  6824  domen  6875  brsdom  6884  brdom2  6891  reuen1  6930  sbthlem10  6980  brsdom2  6985  xpf1o  7023  onfin2  7052  0sdom1dom  7060  modom  7063  unfi  7124  marypha2lem3  7190  dfsup2OLD  7196  wemapso2lem  7265  elom3  7349  dfom5  7351  trcl  7410  epfrs  7413  rankf  7466  scottexs  7557  scott0s  7558  cplem1  7559  karden  7565  hta  7567  pm54.43lem  7632  alephsuc2  7707  iscard3  7720  aceq0  7745  aceq3lem  7747  dfac3  7748  dfac5lem2  7751  dfac5  7755  dfac7  7758  dfac12a  7774  kmlem12  7787  kmlem14  7789  kmlem15  7790  infmap2  7844  ackbij2  7869  ominf4  7938  dfacfin7  8025  ituniiun  8048  zorng  8131  brdom7disj  8156  entri2  8180  alephreg  8204  fpwwe2lem12  8263  fpwwe2lem13  8264  pwfseqlem1  8280  grutsk  8444  axgroth4  8454  grothprim  8456  grothtsk  8457  elni2  8501  ltsopi  8512  genpass  8633  psslinpr  8655  ltexprlem4  8663  ltresr  8762  1re  8837  infm3  9713  elnnz  10034  dfz2  10041  2rexuz  10271  nnwos  10286  eluz2b1  10289  qexALT  10331  elxr  10458  dflt2  10482  xrsupss  10627  xrinfmss  10628  elixx1  10665  elioo2  10697  elioopnf  10737  elicopnf  10739  elfz1  10787  fznn0  10851  fznn  10852  nn0opthlem1  11283  faclbnd4lem1  11306  hashf  11344  hashfun  11389  hashf1  11395  fz1isolem  11399  shftdm  11566  rediv  11616  imdiv  11623  rexanre  11830  caubnd  11842  climreu  12030  dvdslelem  12573  bitsval  12615  smueqlem  12681  algcvgblem  12747  isprm2  12766  isprm3  12767  isprm4  12768  pythagtriplem2  12870  elgz  12978  hashbc0  13052  0ram  13067  isstruct  13158  issect  13656  isssc  13697  isfull2  13785  isfth2  13789  fucinv  13847  eldmcoa  13897  isdrs  14068  fpwipodrs  14267  submacs  14442  isnsg4  14660  isgim  14726  gaorb  14761  oppgid  14829  oppgsubm  14835  oppgcntz  14837  ispgp  14903  efgsdm  15039  efgcpbllema  15063  iscyg2  15169  isrng  15345  isirred2  15483  opprirred  15484  dfrhm2  15498  drngid2  15528  opprsubrg  15566  islmod  15631  lss1d  15720  islmhm  15784  islmim  15815  lbsextlem2  15912  lidlnz  15980  lidldvgen  16007  isnzr2  16015  isassa  16056  dfprm2  16447  isphl  16532  elocv  16568  iunocv  16581  isobs  16620  isbasis3g  16687  fctop  16741  cctop  16743  isclo2  16825  restsn  16901  lmbr  16988  ist0-3  17073  2ndcdisj  17182  1stccnp  17188  1stckgenlem  17248  txbas  17262  ptbasin  17272  tx2cn  17304  fbfinnfr  17536  fbasrn  17579  filuni  17580  ufinffr  17624  fin1aufil  17627  rnelfmlem  17647  flimrest  17678  alexsubALTlem3  17743  alexsubALTlem4  17744  tgphaus  17799  istlm  17867  isngp2  18119  isnlm  18186  elcncf1di  18399  isphtpc  18492  phtpcer  18493  om1elbas  18530  isclm  18562  iscph  18606  iscau3  18704  minveclem3b  18792  elovolm  18834  ioombl1lem4  18918  dyaddisj  18951  vitali  18968  itg1climres  19069  itg2seq  19097  itg2monolem1  19105  itg2mono  19108  limcrcl  19224  lhop1  19361  itgsubst  19396  isuc1p  19526  ismon1p  19528  plydivex  19677  ellogdm  19986  1cubr  20138  atandm2  20173  birthdaylem3  20248  dmarea  20252  dchrelbas2  20476  dchrelbas4  20482  isgrpo2  20864  nmoubi  21350  nmobndseqi  21357  nmobndseqiOLD  21358  minvecolem1  21453  isch2  21803  hlimreui  21819  isch3  21821  ocsh  21862  dfch2  21986  spanuni  22123  nonbooli  22230  5oalem7  22239  adjsym  22413  elbdop2  22451  dmadjss  22467  nmopub  22488  nmfnleub  22505  nmop0h  22571  pjssposi  22752  pjordi  22753  cvbr2  22863  cvnbtwn2  22867  mdsl2i  22902  cvmdi  22904  elat2  22920  atom1d  22933  chirredi  22974  cdj3i  23021  ballotlem2  23047  ballotlemodife  23056  or3di  23123  rabid2f  23135  2reuswap2  23137  rexunirn  23140  mo5f  23143  iuneq12daf  23154  iuneq12df  23155  iuninc  23158  disjex  23176  disjexc  23177  rabfmpunirn  23217  mptfnf  23226  funcnv5mpt  23236  eliccelico  23270  elicoelioo  23271  disjorf  23356  hasheuni  23453  pwsiga  23491  sigainb  23497  2ndmbfm  23566  isibfm  23593  probun  23622  erdszelem9  23730  erdszelem10  23731  pconcon  23762  cvmliftiota  23832  nepss  24072  dfso2  24111  dfpo2  24112  dfres3  24116  elrn3  24120  elpotr  24137  dfon2lem3  24141  dfon2lem5  24143  dfon2lem7  24145  dfon2lem8  24146  predreseq  24179  cbvsetlike  24181  dffr4  24182  preduz  24200  wfi  24207  frind  24243  soseq  24254  wfrlem5  24260  wfrlem8  24263  wfrlem11  24266  frrlem5  24285  frrlem5c  24287  elno3  24309  nosgnn0  24312  nocvxminlem  24344  nofulllem5  24360  symdifass  24371  brtxp2  24421  brpprod3a  24426  eltrans  24431  dfon3  24432  elfuns  24454  brsingle  24456  brsuccf  24480  funpartfun  24481  axcontlem7  24598  cgrxfr  24678  segletr  24737  outsideoftr  24752  df3nandALT1  24835  dfdir2  25291  ishomc  25789  isconcl7a  26105  isibcg  26191  cnvresimaOLD  26226  islocfin  26296  neifg  26320  filnetlem4  26330  fdc  26455  nninfnub  26461  prdstotbnd  26518  isdrngo1  26587  ispridl  26659  ismaxidl  26665  prter1  26747  raldifsni  26753  rexrabdioph  26875  dford4  27122  islinds  27279  issdrg  27505  isdomn3  27523  pm11.52  27585  pm11.58  27589  pm13.192  27610  conss34  27645  stoweidlem52  27801  rmoanim  27957  2rmoswap  27962  f1oun2prg  28076  mpt2xopynvov0g  28080  frgra3v  28180  impexp3acom3r  28277  opelopab4  28317  uunT12p1  28575  uunT12p2  28576  uunT12p3  28577  uun2221  28588  uun2221p1  28589  uun2221p2  28590  undif3VD  28658  onfrALTlem5VD  28661  bnj252  28728  bnj253  28729  bnj255  28730  bnj345  28739  bnj133  28753  bnj976  28809  bnj1098  28815  bnj121  28902  bnj130  28906  bnj150  28908  bnj581  28940  bnj607  28948  bnj865  28955  bnj917  28966  bnj934  28967  bnj964  28975  bnj983  28983  bnj996  28987  bnj1021  28996  bnj1033  28999  bnj1047  29003  bnj1049  29004  bnj1090  29009  bnj1128  29020  bnj1175  29034  bnj1189  29039  bnj1204  29042  bnj1253  29047  bnj1312  29088  anandii  29107  islshp  29169  islshpat  29207  lcvbr2  29212  lcvnbtwn2  29217  cvrnbtwn3  29466  isatl  29489  ishlat1  29542  ishlat2  29543  cvrat4  29632  pmapglbx  29958  lhpexle3  30201  dib1dim  31355  diblsmopel  31361  lcfls1lem  31724
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