MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitri Structured version   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  1318  trunanfal  1364  falxortru  1369  nic-axALT  1448  tbw-bijust  1472  rb-bijust  1523  19.43  1615  19.43OLD  1616  excom13  1758  nf4  1891  19.12vv  1921  3exdistr  1933  4exdistrOLD  1935  eeeanv  1938  eeeanvOLD  1939  ee4anv  1940  sbn  2117  sb3an  2144  sbnf2  2183  sb8eu  2298  2eu4  2363  2eu7  2366  2eu8  2367  r19.26-3  2832  rexcom13  2862  cbvreu  2922  ceqsex2  2984  ceqsex4v  2987  ralrab2  3092  rexrab2  3094  reu2  3114  rmo4  3119  reu8  3122  2reu5lem3  3133  rmo2  3238  rmo3  3240  dfss2  3329  ss2rab  3411  rabss  3412  ssrab  3413  dfss4  3567  undi  3580  undif3  3594  difin2  3595  dfnul2  3622  disj  3660  disj4  3668  elimif  3760  disjsn  3860  ssunpr  3953  sspr  3954  sstp  3955  uni0b  4032  uni0c  4033  ssint  4058  iunss  4124  iundif2  4150  disjor  4188  nfnid  4385  ssextss  4409  eqvinop  4433  opcom  4442  opeqsn  4444  opeqpr  4445  brabsbOLD  4456  brabsb  4458  opelopabf  4471  dfid3  4491  pofun  4511  sotrieq  4522  uniuni  4708  reusv2lem4  4719  dflim3  4819  dfom2  4839  opeliunxp  4921  xpiundi  4924  brinxp2  4931  ssrel  4956  reliun  4987  cnvuni  5049  dmopab3  5074  opelres  5143  elres  5173  elsnres  5174  asymref2  5243  intirr  5244  xpeq0  5285  ssrnres  5301  dminxp  5303  dfrel4v  5314  dmsnn0  5327  elxp4  5349  elxp5  5350  rnco  5368  sb8iota  5417  dffun2  5456  fun11  5508  isarep1  5524  dff1o4  5674  fnressn  5910  opabex3d  5981  opabex3  5982  dff1o6  6005  fliftel  6023  oprabid  6097  mpt22eqb  6171  ralrnmpt2  6176  exopxfr  6402  xporderlem  6449  fvopab5  6526  opabiota  6530  tz7.48lem  6690  seqomlem2  6700  oaord  6782  oeeu  6838  nnaord  6854  ecid  6961  mptelixpg  7091  elixpsn  7093  mapsnen  7176  xpsnen  7184  xpcomco  7190  xpassen  7194  omxpenlem  7201  dom0  7227  modom  7301  dfsup2OLD  7440  tz9.12lem3  7707  rankxpsuc  7798  cp  7807  cardprclem  7858  infxpenlem  7887  dfac5lem1  7996  dfac5lem2  7997  dfac5lem5  8000  dfac10c  8010  kmlem3  8024  kmlem12  8033  kmlem13  8034  kmlem14  8035  kmlem15  8036  ackbij2  8115  cflim2  8135  dffin7-2  8270  dfacfin7  8271  fin1a2lem12  8283  axdc3lem3  8324  cfpwsdom  8451  recmulnq  8833  genpass  8878  psslinpr  8900  suplem2pr  8922  opelreal  8997  ltxrlt  9138  addid1  9238  fimaxre  9947  elnn0  10215  elnn0z  10286  nnwos  10536  elxr  10708  xrnepnf  10711  elfzuzb  11045  4fvwrd4  11113  elfzo2  11135  sqeqori  11485  fsumcom2  12550  rpnnen2  12817  gcdcllem1  13003  isprm2  13079  pythagtriplem2  13183  infpn2  13273  4sqlem12  13316  eldmcoa  14212  oduposb  14555  gsumwspan  14783  isnsg2  14962  isnsg4  14975  efgcpbllemb  15379  dmdprd  15551  dprdval  15553  dprdw  15560  dprd2d2  15594  dfrhm2  15813  issubrg  15860  islmim  16126  lbsextlem2  16223  opsrtoslem1  16536  pjfval2  16928  istps3OLD  16979  ntreq0  17133  cmpsub  17455  2ndcdisj  17511  txbas  17591  elpt  17596  txkgen  17676  xkococn  17684  fbun  17864  trfil2  17911  fin1aufil  17956  alexsubALTlem3  18072  cnextcn  18090  divstgplem  18142  eltsms  18154  ustn0  18242  fmucndlem  18313  metrest  18546  restmetu  18609  srabn  19306  ellogdm  20522  1cubr  20674  leibpilem2  20773  dmarea  20788  vmasum  20992  dchrelbas2  21013  trls  21528  4cycl4v4e  21645  4cycl4dv4e  21647  h2hcau  22474  h2hlm  22475  axhcompl-zf  22493  shlesb1i  22880  shne0i  22942  chnlei  22979  cmbr2i  23090  pjneli  23217  ho02i  23324  adjsym  23328  adjeu  23384  lnopeqi  23503  largei  23762  atoml2i  23878  cdj3lem3b  23935  or3di  23943  mo5f  23964  rmo3f  23974  rmo4fOLD  23975  elim2if  23997  disjorf  24013  ofpreima  24073  1stpreima  24087  2ndpreima  24088  xrdifh  24135  ind1a  24410  elunirnmbfm  24595  ballotlemodife  24747  cvmlift2lem1  24981  3orit  25161  fprodcom2  25300  brtp  25364  dftr6  25365  dfpo2  25370  eldm3  25377  elrn3  25378  elima4  25396  19.12b  25421  sspred  25439  predreseq  25446  preduz  25467  wfi  25474  frind  25510  nofulllem5  25653  brtxp  25717  brtxp2  25718  brpprod  25722  brpprod3a  25723  elfix  25740  dffix2  25742  ellimits  25747  dffun10  25751  elfuns  25752  elsingles  25755  brimg  25774  brapply  25775  brsuccf  25778  funpartlem  25779  brrestrict  25786  dfrdg4  25787  tfrqfree  25788  brlb  25792  altopthc  25808  altopthd  25809  axlowdimlem13  25885  axeuclidlem  25893  fvtransport  25958  hfext  26116  df3nandALT2  26139  areacirclem6  26287  filnetlem4  26401  isbnd2  26483  prtlem70  26689  prtlem16  26709  raldifsni  26725  coeq0  26801  fz1eqin  26818  7rexfrabdioph  26851  rmydioph  27076  dford4  27091  pm13.196a  27582  2reu7  27936  2reu8  27937  dfdfat2  27962  aovov0bi  28027  el2xptp  28050  f13dfv  28067  usgra2pth0  28265  el2wlkonotot0  28292  usg2spthonot0  28309  frgra3v  28329  usg2spot2nb  28391  eelT11  28748  eelTT1  28754  eelT01  28755  eel0T1  28756  uunTT1  28842  uunTT1p1  28843  uunTT1p2  28844  uunT11  28845  uunT11p1  28846  uunT11p2  28847  uun111  28854  bnj250  29002  bnj334  29014  bnj345  29015  bnj89  29023  bnj115  29027  bnj919  29073  bnj1304  29128  bnj92  29170  bnj124  29179  bnj126  29181  bnj154  29186  bnj155  29187  bnj523  29195  bnj526  29196  bnj540  29200  bnj581  29216  bnj916  29241  bnj929  29244  bnj964  29251  bnj978  29257  bnj983  29259  bnj1039  29277  bnj1040  29278  bnj1123  29292  bnj1128  29296  bnj1398  29340  sbnf2NEW7  29545  sb3anNEW7  29577  excom13OLD7  29632  19.12vvOLD7  29638  eeeanvOLD7  29641  ee4anvOLD7  29642  ishlat2  30088  polval2N  30640  dicelval3  31915  mapdordlem1a  32369
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