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

Theorem 3bitri 264
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 242 . 2  |-  ( ps  <->  th )
51, 4bitri 242 1  |-  ( ph  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 178
This theorem is referenced by:  bibi1i  307  orbi1i  508  orass  512  or32  515  pm5.32  619  an32  775  excxor  1319  trunanfal  1365  falxortru  1370  nic-axALT  1449  tbw-bijust  1473  rb-bijust  1524  19.43  1617  19.43OLD  1618  excom13  1761  nf4  1894  19.12vv  1925  3exdistr  1937  4exdistrOLD  1939  eeeanv  1942  eeeanvOLD  1943  ee4anv  1944  sbn  2135  sb3an  2146  sbnf2  2191  sb8eu  2306  2eu4  2371  2eu7  2374  2eu8  2375  r19.26-3  2847  rexcom13  2877  cbvreu  2939  ceqsex2  3001  ceqsex4v  3004  ralrab2  3109  rexrab2  3111  reu2  3131  rmo4  3136  reu8  3139  2reu5lem3  3150  sbc3an  3231  rmo2  3265  rmo3  3267  dfss2  3326  ss2rab  3408  rabss  3409  ssrab  3410  dfss4  3563  undi  3576  undif3  3590  difin2  3591  dfnul2  3618  disj  3696  disj4  3704  elimif  3795  disjsn  3897  ssunpr  3990  sspr  3991  sstp  3992  uni0b  4069  uni0c  4070  ssint  4095  iunss  4162  iundif2  4188  disjor  4227  nfnid  4428  ssextss  4452  eqvinop  4476  opcom  4485  opeqsn  4487  opeqpr  4488  brabsbOLD  4499  brabsb  4501  opelopabf  4514  dfid3  4534  pofun  4554  sotrieq  4565  uniuni  4751  reusv2lem4  4762  dflim3  4862  dfom2  4882  opeliunxp  4964  xpiundi  4967  brinxp2  4974  ssrel  4999  reliun  5030  cnvuni  5092  dmopab3  5117  opelres  5186  elres  5216  elsnres  5217  asymref2  5286  intirr  5287  xpeq0  5328  ssrnres  5344  dminxp  5346  dfrel4v  5357  dmsnn0  5370  elxp4  5392  elxp5  5393  rnco  5411  sb8iota  5460  dffun2  5499  fun11  5551  isarep1  5567  dff1o4  5717  fnressn  5954  opabex3d  6025  opabex3  6026  dff1o6  6049  fliftel  6067  oprabid  6141  mpt22eqb  6215  ralrnmpt2  6220  exopxfr  6446  xporderlem  6493  fvopab5  6570  opabiota  6574  tz7.48lem  6734  seqomlem2  6744  oaord  6826  oeeu  6882  nnaord  6898  ecid  7005  mptelixpg  7135  elixpsn  7137  mapsnen  7220  xpsnen  7228  xpcomco  7234  xpassen  7238  omxpenlem  7245  dom0  7271  modom  7345  dfsup2OLD  7484  tz9.12lem3  7751  rankxpsuc  7844  cp  7853  cardprclem  7904  infxpenlem  7933  dfac5lem1  8042  dfac5lem2  8043  dfac5lem5  8046  dfac10c  8056  kmlem3  8070  kmlem12  8079  kmlem13  8080  kmlem14  8081  kmlem15  8082  ackbij2  8161  cflim2  8181  dffin7-2  8316  dfacfin7  8317  fin1a2lem12  8329  axdc3lem3  8370  cfpwsdom  8497  recmulnq  8879  genpass  8924  psslinpr  8946  suplem2pr  8968  opelreal  9043  ltxrlt  9184  addid1  9284  fimaxre  9993  elnn0  10261  elnn0z  10332  nnwos  10582  elxr  10754  xrnepnf  10757  elfzuzb  11091  4fvwrd4  11159  elfzo2  11181  sqeqori  11531  fsumcom2  12596  rpnnen2  12863  gcdcllem1  13049  isprm2  13125  pythagtriplem2  13229  infpn2  13319  4sqlem12  13362  eldmcoa  14258  oduposb  14601  gsumwspan  14829  isnsg2  15008  isnsg4  15021  efgcpbllemb  15425  dmdprd  15597  dprdval  15599  dprdw  15606  dprd2d2  15640  dfrhm2  15859  issubrg  15906  islmim  16172  lbsextlem2  16269  opsrtoslem1  16582  pjfval2  16974  istps3OLD  17025  ntreq0  17179  cmpsub  17501  2ndcdisj  17557  txbas  17637  elpt  17642  txkgen  17722  xkococn  17730  fbun  17910  trfil2  17957  fin1aufil  18002  alexsubALTlem3  18118  cnextcn  18136  divstgplem  18188  eltsms  18200  ustn0  18288  fmucndlem  18359  metrest  18592  restmetu  18655  srabn  19352  ellogdm  20568  1cubr  20720  leibpilem2  20819  dmarea  20834  vmasum  21038  dchrelbas2  21059  trls  21574  4cycl4v4e  21691  4cycl4dv4e  21693  h2hcau  22520  h2hlm  22521  axhcompl-zf  22539  shlesb1i  22926  shne0i  22988  chnlei  23025  cmbr2i  23136  pjneli  23263  ho02i  23370  adjsym  23374  adjeu  23430  lnopeqi  23549  largei  23808  atoml2i  23924  cdj3lem3b  23981  or3di  23989  mo5f  24008  rmo3f  24018  rmo4fOLD  24019  elim2if  24041  disjorf  24056  ofpreima  24116  1stpreima  24130  2ndpreima  24131  xrdifh  24178  ind1a  24453  elunirnmbfm  24638  ballotlemodife  24790  cvmlift2lem1  25024  3orit  25204  fprodcom2  25343  brtp  25407  dftr6  25408  dfpo2  25413  eldm3  25420  elrn3  25421  elima4  25439  19.12b  25464  sspred  25482  predreseq  25489  preduz  25510  wfi  25517  frind  25553  nofulllem5  25696  brtxp  25760  brtxp2  25761  brpprod  25765  brpprod3a  25766  elfix  25783  dffix2  25785  ellimits  25790  dffun10  25794  elfuns  25795  elsingles  25798  brimg  25817  brapply  25818  brsuccf  25821  funpartlem  25822  brrestrict  25829  dfrdg4  25830  tfrqfree  25831  brlb  25835  altopthc  25851  altopthd  25852  axlowdimlem13  25928  axeuclidlem  25936  fvtransport  26001  hfext  26159  df3nandALT2  26182  areacirclem5  26338  filnetlem4  26452  isbnd2  26534  prtlem70  26812  prtlem16  26830  raldifsni  26846  coeq0  26922  fz1eqin  26939  7rexfrabdioph  26972  rmydioph  27197  dford4  27212  pm13.196a  27703  2reu7  28057  2reu8  28058  dfdfat2  28083  aovov0bi  28148  el2xptp  28173  f13dfv  28197  usgra2pth0  28448  el2wlkonotot0  28502  usg2spthonot0  28519  frgra3v  28564  usg2spot2nb  28626  eelT11  28983  eelTT1  28989  eelT01  28990  eel0T1  28991  uunTT1  29077  uunTT1p1  29078  uunTT1p2  29079  uunT11  29080  uunT11p1  29081  uunT11p2  29082  uun111  29089  bnj250  29239  bnj334  29251  bnj345  29252  bnj89  29260  bnj115  29264  bnj919  29310  bnj1304  29365  bnj92  29407  bnj124  29416  bnj126  29418  bnj154  29423  bnj155  29424  bnj523  29432  bnj526  29433  bnj540  29437  bnj581  29453  bnj916  29478  bnj929  29481  bnj964  29488  bnj978  29494  bnj983  29496  bnj1039  29514  bnj1040  29515  bnj1123  29529  bnj1128  29533  bnj1398  29577  sbnf2NEW7  29782  sb3anNEW7  29814  excom13OLD7  29869  19.12vvOLD7  29875  eeeanvOLD7  29878  ee4anvOLD7  29879  ishlat2  30325  polval2N  30877  dicelval3  32152  mapdordlem1a  32606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator