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  2127  sbnf2  2165  sb8eu  2280  2eu4  2345  2eu7  2348  2eu8  2349  r19.26-3  2808  rexcom13  2838  cbvreu  2898  ceqsex2  2960  ceqsex4v  2963  ralrab2  3068  rexrab2  3070  reu2  3090  rmo4  3095  reu8  3098  2reu5lem3  3109  rmo2  3214  rmo3  3216  dfss2  3305  ss2rab  3387  rabss  3388  ssrab  3389  dfss4  3543  undi  3556  undif3  3570  difin2  3571  dfnul2  3598  disj  3636  disj4  3644  elimif  3736  disjsn  3836  ssunpr  3929  sspr  3930  sstp  3931  uni0b  4008  uni0c  4009  ssint  4034  iunss  4100  iundif2  4126  disjor  4164  nfnid  4361  ssextss  4385  eqvinop  4409  opcom  4418  opeqsn  4420  opeqpr  4421  brabsbOLD  4432  brabsb  4434  opelopabf  4447  dfid3  4467  pofun  4487  sotrieq  4498  uniuni  4683  reusv2lem4  4694  dflim3  4794  dfom2  4814  opeliunxp  4896  xpiundi  4899  brinxp2  4906  ssrel  4931  reliun  4962  cnvuni  5024  dmopab3  5049  opelres  5118  elres  5148  elsnres  5149  asymref2  5218  intirr  5219  xpeq0  5260  ssrnres  5276  dminxp  5278  dfrel4v  5289  dmsnn0  5302  elxp4  5324  elxp5  5325  rnco  5343  sb8iota  5392  dffun2  5431  fun11  5483  isarep1  5499  dff1o4  5649  fnressn  5885  opabex3d  5956  opabex3  5957  dff1o6  5980  fliftel  5998  oprabid  6072  mpt22eqb  6146  ralrnmpt2  6151  exopxfr  6377  xporderlem  6424  fvopab5  6501  opabiota  6505  tz7.48lem  6665  seqomlem2  6675  oaord  6757  oeeu  6813  nnaord  6829  ecid  6936  mptelixpg  7066  elixpsn  7068  mapsnen  7151  xpsnen  7159  xpcomco  7165  xpassen  7169  omxpenlem  7176  dom0  7202  modom  7276  dfsup2OLD  7414  tz9.12lem3  7679  rankxpsuc  7770  cp  7779  cardprclem  7830  infxpenlem  7859  dfac5lem1  7968  dfac5lem2  7969  dfac5lem5  7972  dfac10c  7982  kmlem3  7996  kmlem12  8005  kmlem13  8006  kmlem14  8007  kmlem15  8008  ackbij2  8087  cflim2  8107  dffin7-2  8242  dfacfin7  8243  fin1a2lem12  8255  axdc3lem3  8296  cfpwsdom  8423  recmulnq  8805  genpass  8850  psslinpr  8872  suplem2pr  8894  opelreal  8969  ltxrlt  9110  addid1  9210  fimaxre  9919  elnn0  10187  elnn0z  10258  nnwos  10508  elxr  10680  xrnepnf  10683  elfzuzb  11017  4fvwrd4  11084  elfzo2  11106  sqeqori  11456  fsumcom2  12521  rpnnen2  12788  gcdcllem1  12974  isprm2  13050  pythagtriplem2  13154  infpn2  13244  4sqlem12  13287  eldmcoa  14183  oduposb  14526  gsumwspan  14754  isnsg2  14933  isnsg4  14946  efgcpbllemb  15350  dmdprd  15522  dprdval  15524  dprdw  15531  dprd2d2  15565  dfrhm2  15784  issubrg  15831  islmim  16097  lbsextlem2  16194  opsrtoslem1  16507  pjfval2  16899  istps3OLD  16950  ntreq0  17104  cmpsub  17425  2ndcdisj  17480  txbas  17560  elpt  17565  txkgen  17645  xkococn  17653  fbun  17833  trfil2  17880  fin1aufil  17925  alexsubALTlem3  18041  cnextcn  18059  divstgplem  18111  eltsms  18123  ustn0  18211  fmucndlem  18282  metrest  18515  restmetu  18578  srabn  19275  ellogdm  20491  1cubr  20643  leibpilem2  20742  dmarea  20757  vmasum  20961  dchrelbas2  20982  trls  21497  4cycl4v4e  21614  4cycl4dv4e  21616  h2hcau  22443  h2hlm  22444  axhcompl-zf  22462  shlesb1i  22849  shne0i  22911  chnlei  22948  cmbr2i  23059  pjneli  23186  ho02i  23293  adjsym  23297  adjeu  23353  lnopeqi  23472  largei  23731  atoml2i  23847  cdj3lem3b  23904  or3di  23912  mo5f  23933  rmo3f  23943  rmo4fOLD  23944  elim2if  23966  disjorf  23982  ofpreima  24042  1stpreima  24056  2ndpreima  24057  xrdifh  24104  ind1a  24379  elunirnmbfm  24564  ballotlemodife  24716  cvmlift2lem1  24950  3orit  25130  fprodcom2  25269  brtp  25328  dftr6  25329  dfpo2  25334  eldm3  25341  elrn3  25342  19.12b  25380  sspred  25396  predreseq  25401  preduz  25422  wfi  25429  frind  25465  nofulllem5  25582  brtxp  25642  brtxp2  25643  brpprod  25647  brpprod3a  25648  ellimits  25672  elfuns  25676  elsingles  25679  brimg  25698  brapply  25699  brcup  25700  brcap  25701  brsuccf  25702  funpartlem  25703  brrestrict  25710  dfrdg4  25711  tfrqfree  25712  altopthc  25728  altopthd  25729  axlowdimlem13  25805  axeuclidlem  25813  fvtransport  25878  hfext  26036  df3nandALT2  26059  areacirclem6  26194  filnetlem4  26308  isbnd2  26390  prtlem70  26596  prtlem16  26616  raldifsni  26632  coeq0  26708  fz1eqin  26725  7rexfrabdioph  26758  rmydioph  26983  dford4  26998  pm13.196a  27490  2reu7  27844  2reu8  27845  dfdfat2  27870  aovov0bi  27935  el2xptp  27956  f13dfv  27970  usgra2pth0  28050  el2wlkonotot0  28077  usg2spthonot0  28094  frgra3v  28114  usg2spot2nb  28176  eelT11  28529  eelTT1  28535  eelT01  28536  eel0T1  28537  uunTT1  28623  uunTT1p1  28624  uunTT1p2  28625  uunT11  28626  uunT11p1  28627  uunT11p2  28628  uun111  28635  bnj250  28783  bnj334  28795  bnj345  28796  bnj89  28804  bnj115  28808  bnj919  28854  bnj1304  28909  bnj92  28951  bnj124  28960  bnj126  28962  bnj154  28967  bnj155  28968  bnj523  28976  bnj526  28977  bnj540  28981  bnj581  28997  bnj916  29022  bnj929  29025  bnj964  29032  bnj978  29038  bnj983  29040  bnj1039  29058  bnj1040  29059  bnj1123  29073  bnj1128  29077  bnj1398  29121  sbnf2NEW7  29321  sb3anNEW7  29353  excom13OLD7  29391  19.12vvOLD7  29397  eeeanvOLD7  29400  ee4anvOLD7  29401  ishlat2  29848  polval2N  30400  dicelval3  31675  mapdordlem1a  32129
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