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  6546  ecdmn0  6702  wemapwe  7400  r1pw  7517  adderpqlem  8578  mulerpqlem  8579  lterpq  8594  ltanq  8595  genpass  8633  readdcan  8986  lemuldiv  9635  msq11  9657  avglt2  9950  qbtwnre  10526  iooshf  10728  clim2c  11979  lo1o1  12006  climabs0  12059  reef11  12399  absefib  12478  efieq1re  12479  pc2dvds  12931  pcmpt  12940  subsubc  13727  odmulgid  14867  gexdvds  14895  submcmn2  15135  obslbs  16630  cnntr  17004  cndis  17019  cnindis  17020  cnpdis  17021  lmres  17028  cmpfi  17135  ist0-4  17420  txhmeo  17494  tsmssubm  17825  blin  17970  cncfmet  18412  icopnfcnv  18440  lmmbrf  18688  iscauf  18706  causs  18724  mbfposr  19007  itg2gt0  19115  limcflf  19231  limcres  19236  lhop1  19361  dvdsr1p  19547  vmasum  20455  chpchtsum  20458  bposlem1  20523  dmdmd  22880  funcnvmptOLD  23234  funcnvmpt  23235  xrdifh  23273  eqeelen  24532  areacirclem6  24930  areacirc  24931  ellz1  26846  islssfg  27168  proot1ex  27520  nbgraeledg  28145  lsatfixedN  29199  cdlemg10c  30828  diaglbN  31245  dih1  31476  dihglbcpreN  31490  mapdcv  31850
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