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  1616  19.43OLD  1617  excom13  1759  nf4  1892  19.12vv  1922  3exdistr  1934  4exdistrOLD  1936  eeeanv  1939  eeeanvOLD  1940  ee4anv  1941  sbn  2132  sb3an  2142  sbnf2  2186  sb8eu  2301  2eu4  2366  2eu7  2369  2eu8  2370  r19.26-3  2842  rexcom13  2872  cbvreu  2932  ceqsex2  2994  ceqsex4v  2997  ralrab2  3102  rexrab2  3104  reu2  3124  rmo4  3129  reu8  3132  2reu5lem3  3143  rmo2  3248  rmo3  3250  dfss2  3339  ss2rab  3421  rabss  3422  ssrab  3423  dfss4  3577  undi  3590  undif3  3604  difin2  3605  dfnul2  3632  disj  3670  disj4  3678  elimif  3770  disjsn  3870  ssunpr  3963  sspr  3964  sstp  3965  uni0b  4042  uni0c  4043  ssint  4068  iunss  4134  iundif2  4160  disjor  4199  nfnid  4396  ssextss  4420  eqvinop  4444  opcom  4453  opeqsn  4455  opeqpr  4456  brabsbOLD  4467  brabsb  4469  opelopabf  4482  dfid3  4502  pofun  4522  sotrieq  4533  uniuni  4719  reusv2lem4  4730  dflim3  4830  dfom2  4850  opeliunxp  4932  xpiundi  4935  brinxp2  4942  ssrel  4967  reliun  4998  cnvuni  5060  dmopab3  5085  opelres  5154  elres  5184  elsnres  5185  asymref2  5254  intirr  5255  xpeq0  5296  ssrnres  5312  dminxp  5314  dfrel4v  5325  dmsnn0  5338  elxp4  5360  elxp5  5361  rnco  5379  sb8iota  5428  dffun2  5467  fun11  5519  isarep1  5535  dff1o4  5685  fnressn  5921  opabex3d  5992  opabex3  5993  dff1o6  6016  fliftel  6034  oprabid  6108  mpt22eqb  6182  ralrnmpt2  6187  exopxfr  6413  xporderlem  6460  fvopab5  6537  opabiota  6541  tz7.48lem  6701  seqomlem2  6711  oaord  6793  oeeu  6849  nnaord  6865  ecid  6972  mptelixpg  7102  elixpsn  7104  mapsnen  7187  xpsnen  7195  xpcomco  7201  xpassen  7205  omxpenlem  7212  dom0  7238  modom  7312  dfsup2OLD  7451  tz9.12lem3  7718  rankxpsuc  7811  cp  7820  cardprclem  7871  infxpenlem  7900  dfac5lem1  8009  dfac5lem2  8010  dfac5lem5  8013  dfac10c  8023  kmlem3  8037  kmlem12  8046  kmlem13  8047  kmlem14  8048  kmlem15  8049  ackbij2  8128  cflim2  8148  dffin7-2  8283  dfacfin7  8284  fin1a2lem12  8296  axdc3lem3  8337  cfpwsdom  8464  recmulnq  8846  genpass  8891  psslinpr  8913  suplem2pr  8935  opelreal  9010  ltxrlt  9151  addid1  9251  fimaxre  9960  elnn0  10228  elnn0z  10299  nnwos  10549  elxr  10721  xrnepnf  10724  elfzuzb  11058  4fvwrd4  11126  elfzo2  11148  sqeqori  11498  fsumcom2  12563  rpnnen2  12830  gcdcllem1  13016  isprm2  13092  pythagtriplem2  13196  infpn2  13286  4sqlem12  13329  eldmcoa  14225  oduposb  14568  gsumwspan  14796  isnsg2  14975  isnsg4  14988  efgcpbllemb  15392  dmdprd  15564  dprdval  15566  dprdw  15573  dprd2d2  15607  dfrhm2  15826  issubrg  15873  islmim  16139  lbsextlem2  16236  opsrtoslem1  16549  pjfval2  16941  istps3OLD  16992  ntreq0  17146  cmpsub  17468  2ndcdisj  17524  txbas  17604  elpt  17609  txkgen  17689  xkococn  17697  fbun  17877  trfil2  17924  fin1aufil  17969  alexsubALTlem3  18085  cnextcn  18103  divstgplem  18155  eltsms  18167  ustn0  18255  fmucndlem  18326  metrest  18559  restmetu  18622  srabn  19319  ellogdm  20535  1cubr  20687  leibpilem2  20786  dmarea  20801  vmasum  21005  dchrelbas2  21026  trls  21541  4cycl4v4e  21658  4cycl4dv4e  21660  h2hcau  22487  h2hlm  22488  axhcompl-zf  22506  shlesb1i  22893  shne0i  22955  chnlei  22992  cmbr2i  23103  pjneli  23230  ho02i  23337  adjsym  23341  adjeu  23397  lnopeqi  23516  largei  23775  atoml2i  23891  cdj3lem3b  23948  or3di  23956  mo5f  23977  rmo3f  23987  rmo4fOLD  23988  elim2if  24010  disjorf  24026  ofpreima  24086  1stpreima  24100  2ndpreima  24101  xrdifh  24148  ind1a  24423  elunirnmbfm  24608  ballotlemodife  24760  cvmlift2lem1  24994  3orit  25174  fprodcom2  25313  brtp  25377  dftr6  25378  dfpo2  25383  eldm3  25390  elrn3  25391  elima4  25409  19.12b  25434  sspred  25452  predreseq  25459  preduz  25480  wfi  25487  frind  25523  nofulllem5  25666  brtxp  25730  brtxp2  25731  brpprod  25735  brpprod3a  25736  elfix  25753  dffix2  25755  ellimits  25760  dffun10  25764  elfuns  25765  elsingles  25768  brimg  25787  brapply  25788  brsuccf  25791  funpartlem  25792  brrestrict  25799  dfrdg4  25800  tfrqfree  25801  brlb  25805  altopthc  25821  altopthd  25822  axlowdimlem13  25898  axeuclidlem  25906  fvtransport  25971  hfext  26129  df3nandALT2  26152  areacirclem5  26310  filnetlem4  26424  isbnd2  26506  prtlem70  26712  prtlem16  26732  raldifsni  26748  coeq0  26824  fz1eqin  26841  7rexfrabdioph  26874  rmydioph  27099  dford4  27114  pm13.196a  27605  2reu7  27959  2reu8  27960  dfdfat2  27985  aovov0bi  28050  el2xptp  28075  f13dfv  28099  usgra2pth0  28350  el2wlkonotot0  28404  usg2spthonot0  28421  frgra3v  28466  usg2spot2nb  28528  eelT11  28885  eelTT1  28891  eelT01  28892  eel0T1  28893  uunTT1  28979  uunTT1p1  28980  uunTT1p2  28981  uunT11  28982  uunT11p1  28983  uunT11p2  28984  uun111  28991  bnj250  29139  bnj334  29151  bnj345  29152  bnj89  29160  bnj115  29164  bnj919  29210  bnj1304  29265  bnj92  29307  bnj124  29316  bnj126  29318  bnj154  29323  bnj155  29324  bnj523  29332  bnj526  29333  bnj540  29337  bnj581  29353  bnj916  29378  bnj929  29381  bnj964  29388  bnj978  29394  bnj983  29396  bnj1039  29414  bnj1040  29415  bnj1123  29429  bnj1128  29433  bnj1398  29477  sbnf2NEW7  29682  sb3anNEW7  29714  excom13OLD7  29769  19.12vvOLD7  29775  eeeanvOLD7  29778  ee4anvOLD7  29779  ishlat2  30225  polval2N  30777  dicelval3  32052  mapdordlem1a  32506
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