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

Theorem 3bitri 263
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 241 . 2  |-  ( ps  <->  th )
51, 4bitri 241 1  |-  ( ph  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  bibi1i  306  orbi1i  507  orass  511  or32  514  pm5.32  618  an32  774  excxor  1315  trunanfal  1361  falxortru  1366  nic-axALT  1445  tbw-bijust  1469  rb-bijust  1520  19.43  1612  19.43OLD  1613  excom13  1754  nf4  1887  19.12vv  1917  3exdistr  1929  4exdistrOLD  1931  eeeanv  1934  eeeanvOLD  1935  ee4anv  1936  sb3an  2119  sbnf2  2157  sb8eu  2272  2eu4  2337  2eu7  2340  2eu8  2341  r19.26-3  2800  rexcom13  2830  cbvreu  2890  ceqsex2  2952  ceqsex4v  2955  ralrab2  3060  rexrab2  3062  reu2  3082  rmo4  3087  reu8  3090  2reu5lem3  3101  rmo2  3206  rmo3  3208  dfss2  3297  ss2rab  3379  rabss  3380  ssrab  3381  dfss4  3535  undi  3548  undif3  3562  difin2  3563  dfnul2  3590  disj  3628  disj4  3636  elimif  3728  disjsn  3828  ssunpr  3921  sspr  3922  sstp  3923  uni0b  4000  uni0c  4001  ssint  4026  iunss  4092  iundif2  4118  disjor  4156  nfnid  4353  ssextss  4377  eqvinop  4401  opcom  4410  opeqsn  4412  opeqpr  4413  brabsbOLD  4424  brabsb  4426  opelopabf  4439  dfid3  4459  pofun  4479  sotrieq  4490  uniuni  4675  reusv2lem4  4686  dflim3  4786  dfom2  4806  opeliunxp  4888  xpiundi  4891  brinxp2  4898  ssrel  4923  reliun  4954  cnvuni  5016  dmopab3  5041  opelres  5110  elres  5140  elsnres  5141  asymref2  5210  intirr  5211  xpeq0  5252  ssrnres  5268  dminxp  5270  dfrel4v  5281  dmsnn0  5294  elxp4  5316  elxp5  5317  rnco  5335  sb8iota  5384  dffun2  5423  fun11  5475  isarep1  5491  dff1o4  5641  fnressn  5877  opabex3d  5948  opabex3  5949  dff1o6  5972  fliftel  5990  oprabid  6064  mpt22eqb  6138  ralrnmpt2  6143  exopxfr  6369  xporderlem  6416  fvopab5  6493  opabiota  6497  tz7.48lem  6657  seqomlem2  6667  oaord  6749  oeeu  6805  nnaord  6821  ecid  6928  mptelixpg  7058  elixpsn  7060  mapsnen  7143  xpsnen  7151  xpcomco  7157  xpassen  7161  omxpenlem  7168  dom0  7194  modom  7268  dfsup2OLD  7406  tz9.12lem3  7671  rankxpsuc  7762  cp  7771  cardprclem  7822  infxpenlem  7851  dfac5lem1  7960  dfac5lem2  7961  dfac5lem5  7964  dfac10c  7974  kmlem3  7988  kmlem12  7997  kmlem13  7998  kmlem14  7999  kmlem15  8000  ackbij2  8079  cflim2  8099  dffin7-2  8234  dfacfin7  8235  fin1a2lem12  8247  axdc3lem3  8288  cfpwsdom  8415  recmulnq  8797  genpass  8842  psslinpr  8864  suplem2pr  8886  opelreal  8961  ltxrlt  9102  addid1  9202  fimaxre  9911  elnn0  10179  elnn0z  10250  nnwos  10500  elxr  10672  xrnepnf  10675  elfzuzb  11009  4fvwrd4  11076  elfzo2  11098  sqeqori  11448  fsumcom2  12513  rpnnen2  12780  gcdcllem1  12966  isprm2  13042  pythagtriplem2  13146  infpn2  13236  4sqlem12  13279  eldmcoa  14175  oduposb  14518  gsumwspan  14746  isnsg2  14925  isnsg4  14938  efgcpbllemb  15342  dmdprd  15514  dprdval  15516  dprdw  15523  dprd2d2  15557  dfrhm2  15776  issubrg  15823  islmim  16089  lbsextlem2  16186  opsrtoslem1  16499  pjfval2  16891  istps3OLD  16942  ntreq0  17096  cmpsub  17417  2ndcdisj  17472  txbas  17552  elpt  17557  txkgen  17637  xkococn  17645  fbun  17825  trfil2  17872  fin1aufil  17917  alexsubALTlem3  18033  cnextcn  18051  divstgplem  18103  eltsms  18115  ustn0  18203  fmucndlem  18274  metrest  18507  restmetu  18570  srabn  19267  ellogdm  20483  1cubr  20635  leibpilem2  20734  dmarea  20749  vmasum  20953  dchrelbas2  20974  trls  21489  4cycl4v4e  21606  4cycl4dv4e  21608  h2hcau  22435  h2hlm  22436  axhcompl-zf  22454  shlesb1i  22841  shne0i  22903  chnlei  22940  cmbr2i  23051  pjneli  23178  ho02i  23285  adjsym  23289  adjeu  23345  lnopeqi  23464  largei  23723  atoml2i  23839  cdj3lem3b  23896  or3di  23904  mo5f  23925  rmo3f  23935  rmo4fOLD  23936  elim2if  23958  disjorf  23974  ofpreima  24034  1stpreima  24048  2ndpreima  24049  xrdifh  24096  ind1a  24371  elunirnmbfm  24556  ballotlemodife  24708  cvmlift2lem1  24942  3orit  25122  fprodcom2  25261  brtp  25320  dftr6  25321  dfpo2  25326  eldm3  25333  elrn3  25334  19.12b  25372  sspred  25388  predreseq  25393  preduz  25414  wfi  25421  frind  25457  nofulllem5  25574  brtxp  25634  brtxp2  25635  brpprod  25639  brpprod3a  25640  ellimits  25664  elfuns  25668  elsingles  25671  brimg  25690  brapply  25691  brcup  25692  brcap  25693  brsuccf  25694  funpartlem  25695  brrestrict  25702  dfrdg4  25703  tfrqfree  25704  altopthc  25720  altopthd  25721  axlowdimlem13  25797  axeuclidlem  25805  fvtransport  25870  hfext  26028  df3nandALT2  26051  areacirclem6  26186  filnetlem4  26300  isbnd2  26382  prtlem70  26588  prtlem16  26608  raldifsni  26624  coeq0  26700  fz1eqin  26717  7rexfrabdioph  26750  rmydioph  26975  dford4  26990  pm13.196a  27482  2reu7  27836  2reu8  27837  dfdfat2  27862  aovov0bi  27927  el2xptp  27948  f13dfv  27962  usgra2pth0  28042  el2wlkonotot0  28069  usg2spthonot0  28086  frgra3v  28106  usg2spot2nb  28168  eelT11  28520  eelTT1  28526  eelT01  28527  eel0T1  28528  uunTT1  28614  uunTT1p1  28615  uunTT1p2  28616  uunT11  28617  uunT11p1  28618  uunT11p2  28619  uun111  28626  bnj250  28771  bnj334  28783  bnj345  28784  bnj89  28792  bnj115  28796  bnj919  28842  bnj1304  28897  bnj92  28939  bnj124  28948  bnj126  28950  bnj154  28955  bnj155  28956  bnj523  28964  bnj526  28965  bnj540  28969  bnj581  28985  bnj916  29010  bnj929  29013  bnj964  29020  bnj978  29026  bnj983  29028  bnj1039  29046  bnj1040  29047  bnj1123  29061  bnj1128  29065  bnj1398  29109  sbnf2NEW7  29309  sb3anNEW7  29341  excom13OLD7  29379  19.12vvOLD7  29385  eeeanvOLD7  29388  ee4anvOLD7  29389  ishlat2  29836  polval2N  30388  dicelval3  31663  mapdordlem1a  32117
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