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

Theorem 3bitrd 270
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 244 . 2  |-  ( ph  ->  ( ps  <->  th )
)
4 3bitrd.3 . 2  |-  ( ph  ->  ( th  <->  ta )
)
53, 4bitrd 244 1  |-  ( ph  ->  ( ps  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  sbceqal  3055  sbcnel12g  3111  elimhyp3v  3628  elimhyp4v  3629  keephyp3v  3634  f1eq123d  5483  foeq123d  5484  f1oeq123d  5485  ofrfval  6102  eloprabi  6202  smoeq  6383  wemapwe  7416  cnfcom  7419  fseqenlem1  7667  dfac12lem2  7786  fin23lem22  7969  pwfseqlem5  8301  pwfseq  8302  enqbreq2  8560  lterpq  8610  ltdiv23  9663  lediv23  9664  halfpos  9958  addltmul  9963  supminf  10321  supxrbnd1  10656  supxrbnd2  10657  iccf1o  10794  fzshftral  10885  modirr  11025  seqcoll  11417  s111  11464  limsupgle  11967  tanaddlem  12462  dvdssub  12585  dvdsmod  12601  oddp1even  12605  bitscmp  12645  saddisjlem  12671  smueqlem  12697  prmreclem5  12983  4sqlem11  13018  4sqlem17  13024  vdwmc2  13042  ismre  13508  acsfn  13577  isssc  13713  setcinv  13938  nmzsubg  14674  conjnmzb  14733  oddvdsnn0  14875  oddvds  14878  odcong  14880  odf1  14891  dpjeq  15310  pgpfac1lem2  15326  lsmspsn  15853  lbsacsbs  15925  lpigen  16024  prmirredlem  16462  znf1o  16521  znunit  16533  isclo  16840  maxlp  16894  1stccn  17205  xkoinjcn  17397  elmptrab  17538  fbunfip  17580  elfm  17658  fmid  17671  flfnei  17702  isflf  17704  isfcls  17720  fclsopn  17725  isfcf  17745  eltsms  17831  prdsxmetlem  17948  elmopn  18004  metss  18070  comet  18075  nrmmetd  18113  metdsge  18369  tchcph  18683  fmcfil  18714  minveclem4  18812  shft2rab  18883  sca2rab  18887  volsup2  18976  mbfsup  19035  i1fmullem  19065  mbfi1fseqlem4  19089  xrge0f  19102  itg2monolem1  19121  ellimc2  19243  cnlimc  19254  mdegleb  19466  facth1  19566  ulm2  19780  sineq0  19905  coseq1  19906  efeq1  19907  sinord  19912  root1eq1  20111  angrtmuld  20122  quad2  20151  dcubic  20158  cubic2  20160  dquartlem1  20163  dquart  20165  quart  20173  rlimcnp  20276  mumullem2  20434  chtub  20467  fsumvma  20468  fsumvma2  20469  chpchtsum  20474  bposlem7  20545  lgsneg  20574  lgsne0  20588  lgsqrlem2  20597  lgsquadlem1  20609  lgsquadlem2  20610  isass  20999  rngosn3  21109  imsmetlem  21275  ipz  21311  bnsscmcl  21463  minvecolem4  21475  hvsubcan  21669  hoeq2  22427  leoptri  22732  atcv0eq  22975  fzsplit3  23047  ballotlemsima  23090  elimifd  23167  gtiso  23256  lmlim  23386  dya2ub  23590  isrrvv  23661  subfacp1lem3  23728  subfacp1lem5  23730  erdszelem1  23737  erdsze  23748  erdsze2lem2  23750  eupath2lem2  23917  eupath2lem3  23918  elpredg  24249  axcontlem7  24670  itg2addnclem2  25004  areacirclem2  25028  areacirclem3  25029  areacirclem6  25033  splint  25151  nZdef  25283  islatalg  25286  isfldOLD  25529  svli2  25587  nelioo5  25614  imonclem  25916  cmppar3  26077  isnword  26089  pdiveql  26271  filnetlem4  26433  metf1o  26572  elrfirn  26873  jm2.19lem2  27186  islinds2  27386  islindf4  27411  f1omvdconj  27492  proot1ex  27623  2reu4a  28070  isuslgra  28234  isusgra  28235  nb3graprlem2  28288  cusgra3v  28299  uvtx01vtx  28305  iswlkon  28332  istrlon  28340  0pth  28356  wlkdvspthlem  28365  frgra3v  28426  bnj1452  29398  lsatcv0eq  29859  cmtbr2N  30065  atlatmstc  30131  1cvrco  30283  cdleme3  31048  cdleme7  31060  cdlemg10c  31450  dvhopellsm  31929  dibord  31971  dib1dim2  31980  diblsmopel  31983  dihopelvalcpre  32060  dih1dimatlem  32141  hdmap14lem13  32695  hdmapoc  32746
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 177
  Copyright terms: Public domain W3C validator