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

Theorem 3bitr4rd 277
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr4d.1  |-  ( ph  ->  ( ps  <->  ch )
)
3bitr4d.2  |-  ( ph  ->  ( th  <->  ps )
)
3bitr4d.3  |-  ( ph  ->  ( ta  <->  ch )
)
Assertion
Ref Expression
3bitr4rd  |-  ( ph  ->  ( ta  <->  th )
)

Proof of Theorem 3bitr4rd
StepHypRef Expression
1 3bitr4d.3 . . 3  |-  ( ph  ->  ( ta  <->  ch )
)
2 3bitr4d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2bitr4d 247 . 2  |-  ( ph  ->  ( ta  <->  ps )
)
4 3bitr4d.2 . 2  |-  ( ph  ->  ( th  <->  ps )
)
53, 4bitr4d 247 1  |-  ( ph  ->  ( ta  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  oacan  6562  ecdmn0  6718  wemapwe  7416  r1pw  7533  adderpqlem  8594  mulerpqlem  8595  lterpq  8610  ltanq  8611  genpass  8649  readdcan  9002  lemuldiv  9651  msq11  9673  avglt2  9966  qbtwnre  10542  iooshf  10744  clim2c  11995  lo1o1  12022  climabs0  12075  reef11  12415  absefib  12494  efieq1re  12495  pc2dvds  12947  pcmpt  12956  subsubc  13743  odmulgid  14883  gexdvds  14911  submcmn2  15151  obslbs  16646  cnntr  17020  cndis  17035  cnindis  17036  cnpdis  17037  lmres  17044  cmpfi  17151  ist0-4  17436  txhmeo  17510  tsmssubm  17841  blin  17986  cncfmet  18428  icopnfcnv  18456  lmmbrf  18704  iscauf  18722  causs  18740  mbfposr  19023  itg2gt0  19131  limcflf  19247  limcres  19252  lhop1  19377  dvdsr1p  19563  vmasum  20471  chpchtsum  20474  bposlem1  20539  dmdmd  22896  funcnvmptOLD  23249  funcnvmpt  23250  xrdifh  23288  eqeelen  24604  leceifl  24999  iblabsnclem  25014  areacirclem6  25033  areacirc  25034  ellz1  26949  islssfg  27271  proot1ex  27623  nbgraeledg  28279  nb3graprlem2  28288  cusgra3v  28299  lsatfixedN  29821  cdlemg10c  31450  diaglbN  31867  dih1  32098  dihglbcpreN  32112  mapdcv  32472
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