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

Theorem 3bitri 262
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3bitri.1  |-  ( ph  <->  ps )
3bitri.2  |-  ( ps  <->  ch )
3bitri.3  |-  ( ch  <->  th )
Assertion
Ref Expression
3bitri  |-  ( ph  <->  th )

Proof of Theorem 3bitri
StepHypRef Expression
1 3bitri.1 . 2  |-  ( ph  <->  ps )
2 3bitri.2 . . 3  |-  ( ps  <->  ch )
3 3bitri.3 . . 3  |-  ( ch  <->  th )
42, 3bitri 240 . 2  |-  ( ps  <->  th )
51, 4bitri 240 1  |-  ( ph  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  bibi1i  305  orbi1i  506  orass  510  or32  513  pm5.32  617  an32  773  excxor  1300  trunanfal  1345  falxortru  1350  nic-axALT  1429  tbw-bijust  1453  rb-bijust  1504  19.43  1595  19.43OLD  1596  nf4  1812  excom13  1829  19.12vv  1851  3exdistr  1863  4exdistr  1864  eeeanv  1867  ee4anv  1868  sb3an  2023  sbnf2  2060  sb8eu  2174  2eu4  2239  2eu7  2242  2eu8  2243  r19.26-3  2690  rexcom13  2715  cbvreu  2775  ceqsex2  2837  ceqsex4v  2840  ralrab2  2944  rexrab2  2946  reu2  2966  rmo4  2971  reu8  2974  2reu5lem3  2985  rmo2  3089  rmo3  3091  dfss2  3182  ss2rab  3262  rabss  3263  ssrab  3264  dfss4  3416  undi  3429  undif3  3442  difin2  3443  dfnul2  3470  disj  3508  disj4  3516  elimif  3607  disjsn  3706  ssunpr  3792  sspr  3793  sstp  3794  uni0b  3868  uni0c  3869  ssint  3894  iunss  3959  iundif2  3985  disjor  4023  nfnid  4220  ssextss  4243  eqvinop  4267  opcom  4276  opeqsn  4278  opeqpr  4279  brabsbOLD  4290  brabsb  4292  opelopabf  4305  dfid3  4326  pofun  4346  sotrieq  4357  trsuc2OLD  4493  uniuni  4543  reusv2lem4  4554  dflim3  4654  dfom2  4674  opeliunxp  4756  xpiundi  4759  brinxp2  4767  ssrel  4792  reliun  4822  cnvuni  4882  dmopab3  4907  opelres  4976  elres  5006  elsnres  5007  asymref2  5076  intirr  5077  xpeq0  5116  ssrnres  5132  dminxp  5134  dfrel4v  5141  dmsnn0  5154  elxp4  5176  elxp5  5177  rnco  5195  sb8iota  5242  dffun2  5281  fun11  5331  isarep1  5347  dff1o4  5496  fnressn  5721  opabex3  5785  dff1o6  5807  fliftel  5824  oprabid  5898  mpt22eqb  5969  ralrnmpt2  5974  exopxfr  6199  xporderlem  6242  fvopab5  6305  opabiota  6309  tz7.48lem  6469  seqomlem2  6479  oaord  6561  nnaord  6633  ecid  6740  mptelixpg  6869  elixpsn  6871  mapsnen  6954  xpsnen  6962  xpcomco  6968  xpassen  6972  omxpenlem  6979  dom0  7005  modom  7079  dfsup2OLD  7212  tz9.12lem3  7477  rankxpsuc  7568  cp  7577  cardprclem  7628  infxpenlem  7657  dfac5lem1  7766  dfac5lem2  7767  dfac5lem5  7770  dfac10c  7780  kmlem3  7794  kmlem12  7803  kmlem13  7804  kmlem14  7805  kmlem15  7806  ackbij2  7885  cflim2  7905  dffin7-2  8040  dfacfin7  8041  fin1a2lem12  8053  axdc3lem3  8094  cfpwsdom  8222  recmulnq  8604  genpass  8649  psslinpr  8671  suplem2pr  8693  opelreal  8768  ltxrlt  8909  addid1  9008  fimaxre  9717  elnn0  9983  elnn0z  10052  nnwos  10302  elxr  10474  xrnepnf  10477  elfzuzb  10808  elfzo2  10894  sqeqori  11231  fsumcom2  12253  rpnnen2  12520  gcdcllem1  12706  isprm2  12782  pythagtriplem2  12886  infpn2  12976  4sqlem12  13019  eldmcoa  13913  oduposb  14256  isnsg2  14663  isnsg4  14676  efgcpbllemb  15080  dmdprd  15252  dprdval  15254  dprdw  15261  dprd2d2  15295  dfrhm2  15514  issubrg  15561  islmim  15831  lbsextlem2  15928  opsrtoslem1  16241  pjfval2  16625  istps3OLD  16676  ntreq0  16830  cmpsub  17143  2ndcdisj  17198  txbas  17278  elpt  17283  txkgen  17362  xkococn  17370  fbun  17551  trfil2  17598  fin1aufil  17643  alexsubALTlem3  17759  divstgplem  17819  eltsms  17831  metrest  18086  srabn  18793  ellogdm  20002  1cubr  20154  leibpilem2  20253  dmarea  20268  vmasum  20471  dchrelbas2  20492  h2hcau  21575  h2hlm  21576  axhcompl-zf  21594  shlesb1i  21981  shne0i  22043  chnlei  22080  cmbr2i  22191  pjneli  22318  ho02i  22425  adjsym  22429  adjeu  22485  lnopeqi  22604  largei  22863  atoml2i  22979  cdj3lem3b  23036  ballotlemodife  23072  eliccioo  23131  or3di  23139  mo5f  23159  rmo3f  23194  rmo4fOLD  23195  xrdifh  23288  disjorf  23371  elunirnmbfm  23573  ind1a  23619  cvmlift2lem1  23848  3orit  24081  brtp  24177  dftr6  24178  dfpo2  24183  eldm3  24190  elrn3  24191  19.12b  24229  sspred  24245  predreseq  24250  preduz  24271  wfi  24278  frind  24314  nofulllem5  24431  brtxp  24491  brtxp2  24492  brpprod  24496  brpprod3a  24497  ellimits  24521  elfuns  24525  elsingles  24528  brimg  24547  brapply  24548  brcup  24549  brcap  24550  brsuccf  24551  funpartlem  24552  brrestrict  24559  dfrdg4  24560  tfrqfree  24561  altopthc  24577  altopthd  24578  axlowdimlem13  24654  axeuclidlem  24662  fvtransport  24727  hfext  24885  df3nandALT2  24908  areacirclem6  25033  anddi2  25044  eqvinopb  25068  albineal  25102  dff1o6f  25195  definc  25382  isdir2  25395  bisig0  26165  isibcg  26294  cnvresimaOLD  26329  filnetlem4  26433  isbnd2  26610  prtlem70  26818  prtlem16  26840  raldifsni  26856  coeq0  26934  fz1eqin  26951  7rexfrabdioph  26984  rmydioph  27210  dford4  27225  pm13.196a  27717  compneOLD  27746  2reu7  28072  2reu8  28073  dfdfat2  28099  aovov0bi  28164  opabex3d  28190  4fvwrd4  28220  trls  28335  4cycl4v4e  28412  4cycl4dv4e  28414  frgra3v  28426  eelT11  28788  eelTT1  28794  eelT01  28795  eel0T1  28796  uunTT1  28882  uunTT1p1  28883  uunTT1p2  28884  uunT11  28885  uunT11p1  28886  uunT11p2  28887  uun111  28894  bnj250  29042  bnj334  29054  bnj345  29055  bnj89  29063  bnj115  29067  bnj919  29113  bnj1304  29168  bnj92  29210  bnj124  29219  bnj126  29221  bnj154  29226  bnj155  29227  bnj523  29235  bnj526  29236  bnj540  29240  bnj581  29256  bnj916  29281  bnj929  29284  bnj964  29291  bnj978  29297  bnj983  29299  bnj1039  29317  bnj1040  29318  bnj1123  29332  bnj1128  29336  bnj1398  29380  sbnf2NEW7  29580  sb3anNEW7  29611  excom13OLD7  29649  19.12vvOLD7  29655  eeeanvOLD7  29658  ee4anvOLD7  29659  ishlat2  30165  polval2N  30717  dicelval3  31992  mapdordlem1a  32446
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