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

Theorem 3bitrd 271
Description: Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.)
Hypotheses
Ref Expression
3bitrd.1  |-  ( ph  ->  ( ps  <->  ch )
)
3bitrd.2  |-  ( ph  ->  ( ch  <->  th )
)
3bitrd.3  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
3bitrd  |-  ( ph  ->  ( ps  <->  ta )
)

Proof of Theorem 3bitrd
StepHypRef Expression
1 3bitrd.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
2 3bitrd.2 . . 3  |-  ( ph  ->  ( ch  <->  th )
)
31, 2bitrd 245 . 2  |-  ( ph  ->  ( ps  <->  th )
)
4 3bitrd.3 . 2  |-  ( ph  ->  ( th  <->  ta )
)
53, 4bitrd 245 1  |-  ( ph  ->  ( ps  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  sbceqal  3204  sbcnel12g  3260  elimhyp3v  3781  elimhyp4v  3782  keephyp3v  3787  f1eq123d  5661  foeq123d  5662  f1oeq123d  5663  ofrfval  6305  eloprabi  6405  smoeq  6604  wemapwe  7646  fseqenlem1  7897  dfac12lem2  8016  fin23lem22  8199  pwfseqlem5  8530  pwfseq  8531  enqbreq2  8789  lterpq  8839  ltdiv23  9893  lediv23  9894  halfpos  10190  addltmul  10195  supminf  10555  supxrbnd1  10892  supxrbnd2  10893  iccf1o  11031  fzshftral  11126  modirr  11278  seqcoll  11704  s111  11754  limsupgle  12263  tanaddlem  12759  dvdssub  12882  dvdsmod  12898  oddp1even  12902  bitscmp  12942  saddisjlem  12968  smueqlem  12994  prmreclem5  13280  4sqlem11  13315  4sqlem17  13321  vdwmc2  13339  ismre  13807  acsfn  13876  isssc  14012  setcinv  14237  nmzsubg  14973  conjnmzb  15032  oddvdsnn0  15174  oddvds  15177  odcong  15179  odf1  15190  dpjeq  15609  pgpfac1lem2  15625  lsmspsn  16148  lbsacsbs  16220  lpigen  16319  prmirredlem  16765  znf1o  16824  znunit  16836  isclo  17143  maxlp  17203  1stccn  17518  xkoinjcn  17711  elmptrab  17851  fbunfip  17893  elfm  17971  fmid  17984  flfnei  18015  isflf  18017  isfcls  18033  fclsopn  18038  isfcf  18058  cnextfun  18087  eltsms  18154  prdsxmetlem  18390  elmopn  18464  metss  18530  comet  18535  elbl4  18598  metuel2  18601  nrmmetd  18614  metdsge  18871  tchcph  19186  fmcfil  19217  minveclem4  19325  shft2rab  19396  sca2rab  19400  volsup2  19489  mbfsup  19548  i1fmullem  19578  mbfi1fseqlem4  19602  xrge0f  19615  itg2monolem1  19634  ellimc2  19756  cnlimc  19767  mdegleb  19979  facth1  20079  ulm2  20293  sineq0  20421  coseq1  20422  efeq1  20423  sinord  20428  root1eq1  20631  angrtmuld  20642  quad2  20671  dcubic  20678  cubic2  20680  dquartlem1  20683  dquart  20685  quart  20693  rlimcnp  20796  mumullem2  20955  chtub  20988  fsumvma  20989  fsumvma2  20990  chpchtsum  20995  bposlem7  21066  lgsneg  21095  lgsne0  21109  lgsqrlem2  21118  lgsquadlem1  21130  lgsquadlem2  21131  isuslgra  21364  isusgra  21365  ausisusgra  21372  nb3graprlem2  21453  cusgra3v  21465  sizeusglecusg  21487  uvtx01vtx  21493  is2wlk  21557  0pth  21562  wlkdvspthlem  21599  eupath2lem2  21692  eupath2lem3  21693  isass  21896  rngosn3  22006  imsmetlem  22174  ipz  22210  bnsscmcl  22362  minvecolem4  22374  hvsubcan  22568  hoeq2  23326  leoptri  23631  atcv0eq  23874  elimifd  23996  gtiso  24080  2ndpreima  24088  fzsplit3  24142  isofld  24227  pstmfval  24283  lmlim  24325  dya2ub  24612  isrrvv  24693  ballotlemsima  24765  lgamucov  24814  subfacp1lem3  24860  subfacp1lem5  24862  erdszelem1  24869  erdsze  24880  erdsze2lem2  24882  elpredg  25445  axcontlem7  25901  itg2addnclem2  26247  ftc1anclem1  26270  areacirclem2  26282  areacirclem3  26283  areacirclem6  26287  filnetlem4  26401  metf1o  26452  elrfirn  26740  jm2.19lem2  27052  islinds2  27251  islindf4  27276  f1omvdconj  27357  proot1ex  27488  2reu4a  27934  ltnltne  28079  el2wlkonotot0  28292  el2wlkonotot  28293  el2wlksoton  28298  el2spthsoton  28299  el2wlksot  28300  el2pthsot  28301  frgra3v  28329  usg2spot2nb  28391  bnj1452  29358  lsatcv0eq  29782  cmtbr2N  29988  atlatmstc  30054  1cvrco  30206  cdleme3  30971  cdleme7  30983  cdlemg10c  31373  dvhopellsm  31852  dibord  31894  dib1dim2  31903  diblsmopel  31906  dihopelvalcpre  31983  dih1dimatlem  32064  hdmap14lem13  32618  hdmapoc  32669
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