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  1592  19.43OLD  1593  nf4  1800  excom13  1817  19.12vv  1839  3exdistr  1851  4exdistr  1852  eeeanv  1855  ee4anv  1856  sb3an  2010  sbnf2  2047  sb8eu  2161  2eu4  2226  2eu7  2229  2eu8  2230  r19.26-3  2677  rexcom13  2702  cbvreu  2762  ceqsex2  2824  ceqsex4v  2827  ralrab2  2931  rexrab2  2933  reu2  2953  rmo4  2958  reu8  2961  2reu5lem3  2972  rmo2  3076  rmo3  3078  dfss2  3169  ss2rab  3249  rabss  3250  ssrab  3251  dfss4  3403  undi  3416  undif3  3429  difin2  3430  dfnul2  3457  disj  3495  disj4  3503  elimif  3594  disjsn  3693  ssunpr  3776  sspr  3777  sstp  3778  uni0b  3852  uni0c  3853  ssint  3878  iunss  3943  iundif2  3969  disjor  4007  nfnid  4204  ssextss  4227  eqvinop  4251  opcom  4260  opeqsn  4262  opeqpr  4263  brabsbOLD  4274  brabsb  4276  opelopabf  4289  dfid3  4310  pofun  4330  sotrieq  4341  trsuc2OLD  4477  uniuni  4527  reusv2lem4  4538  dflim3  4638  dfom2  4658  opeliunxp  4740  xpiundi  4743  brinxp2  4751  ssrel  4776  reliun  4806  cnvuni  4866  dmopab3  4891  opelres  4960  elres  4990  elsnres  4991  asymref2  5060  intirr  5061  xpeq0  5100  ssrnres  5116  dminxp  5118  dfrel4v  5125  dmsnn0  5138  elxp4  5160  elxp5  5161  rnco  5179  sb8iota  5226  dffun2  5265  fun11  5315  isarep1  5331  dff1o4  5480  fnressn  5705  opabex3  5769  dff1o6  5791  fliftel  5808  oprabid  5882  mpt22eqb  5953  ralrnmpt2  5958  exopxfr  6183  xporderlem  6226  fvopab5  6289  opabiota  6293  tz7.48lem  6453  seqomlem2  6463  oaord  6545  nnaord  6617  ecid  6724  mptelixpg  6853  elixpsn  6855  mapsnen  6938  xpsnen  6946  xpcomco  6952  xpassen  6956  omxpenlem  6963  dom0  6989  modom  7063  dfsup2OLD  7196  tz9.12lem3  7461  rankxpsuc  7552  cp  7561  cardprclem  7612  infxpenlem  7641  dfac5lem1  7750  dfac5lem2  7751  dfac5lem5  7754  dfac10c  7764  kmlem3  7778  kmlem12  7787  kmlem13  7788  kmlem14  7789  kmlem15  7790  ackbij2  7869  cflim2  7889  dffin7-2  8024  dfacfin7  8025  fin1a2lem12  8037  axdc3lem3  8078  cfpwsdom  8206  recmulnq  8588  genpass  8633  psslinpr  8655  suplem2pr  8677  opelreal  8752  ltxrlt  8893  addid1  8992  fimaxre  9701  elnn0  9967  elnn0z  10036  nnwos  10286  elxr  10458  xrnepnf  10461  elfzuzb  10792  elfzo2  10878  sqeqori  11215  fsumcom2  12237  rpnnen2  12504  gcdcllem1  12690  isprm2  12766  pythagtriplem2  12870  infpn2  12960  4sqlem12  13003  eldmcoa  13897  oduposb  14240  isnsg2  14647  isnsg4  14660  efgcpbllemb  15064  dmdprd  15236  dprdval  15238  dprdw  15245  dprd2d2  15279  dfrhm2  15498  issubrg  15545  islmim  15815  lbsextlem2  15912  opsrtoslem1  16225  pjfval2  16609  istps3OLD  16660  ntreq0  16814  cmpsub  17127  2ndcdisj  17182  txbas  17262  elpt  17267  txkgen  17346  xkococn  17354  fbun  17535  trfil2  17582  fin1aufil  17627  alexsubALTlem3  17743  divstgplem  17803  eltsms  17815  metrest  18070  srabn  18777  ellogdm  19986  1cubr  20138  leibpilem2  20237  dmarea  20252  vmasum  20455  dchrelbas2  20476  h2hcau  21559  h2hlm  21560  axhcompl-zf  21578  shlesb1i  21965  shne0i  22027  chnlei  22064  cmbr2i  22175  pjneli  22302  ho02i  22409  adjsym  22413  adjeu  22469  lnopeqi  22588  largei  22847  atoml2i  22963  cdj3lem3b  23020  ballotlemodife  23056  eliccioo  23115  or3di  23123  mo5f  23143  rmo3f  23178  rmo4fOLD  23179  xrdifh  23273  disjorf  23356  elunirnmbfm  23558  ind1a  23604  cvmlift2lem1  23833  3orit  24066  brtp  24106  dftr6  24107  dfpo2  24112  eldm3  24119  elrn3  24120  19.12b  24158  sspred  24174  predreseq  24179  preduz  24200  wfi  24207  frind  24243  nofulllem5  24360  brtxp  24420  brtxp2  24421  brpprod  24425  brpprod3a  24426  ellimits  24450  elfuns  24454  elsingles  24457  brimg  24476  brapply  24477  brcup  24478  brcap  24479  brsuccf  24480  funpartfun  24481  brrestrict  24487  dfrdg4  24488  tfrqfree  24489  altopthc  24505  altopthd  24506  axlowdimlem13  24582  axeuclidlem  24590  fvtransport  24655  hfext  24813  df3nandALT2  24836  areacirclem6  24930  anddi2  24941  eqvinopb  24965  albineal  24999  dff1o6f  25092  definc  25279  isdir2  25292  bisig0  26062  isibcg  26191  cnvresimaOLD  26226  filnetlem4  26330  isbnd2  26507  prtlem70  26715  prtlem16  26737  raldifsni  26753  coeq0  26831  fz1eqin  26848  7rexfrabdioph  26881  rmydioph  27107  dford4  27122  pm13.196a  27614  compneOLD  27643  2reu7  27969  2reu8  27970  dfdfat2  27994  aovov0bi  28056  frgra3v  28180  eelT11  28483  eelTT1  28488  eelT01  28489  eel0T1  28490  uunTT1  28568  uunTT1p1  28569  uunTT1p2  28570  uunT11  28571  uunT11p1  28572  uunT11p2  28573  uun111  28580  bnj250  28726  bnj334  28738  bnj345  28739  bnj89  28747  bnj115  28751  bnj919  28797  bnj1304  28852  bnj92  28894  bnj124  28903  bnj126  28905  bnj154  28910  bnj155  28911  bnj523  28919  bnj526  28920  bnj540  28924  bnj581  28940  bnj916  28965  bnj929  28968  bnj964  28975  bnj978  28981  bnj983  28983  bnj1039  29001  bnj1040  29002  bnj1123  29016  bnj1128  29020  bnj1398  29064  ishlat2  29543  polval2N  30095  dicelval3  31370  mapdordlem1a  31824
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