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

Theorem 3bitr4rd 279
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 249 . 2  |-  ( ph  ->  ( ta  <->  ps )
)
4 3bitr4d.2 . 2  |-  ( ph  ->  ( th  <->  ps )
)
53, 4bitr4d 249 1  |-  ( ph  ->  ( ta  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  inimasn  5291  oacan  6793  ecdmn0  6949  wemapwe  7656  r1pw  7773  adderpqlem  8833  mulerpqlem  8834  lterpq  8849  ltanq  8850  genpass  8888  readdcan  9242  lemuldiv  9891  msq11  9913  avglt2  10208  qbtwnre  10787  iooshf  10991  clim2c  12301  lo1o1  12328  climabs0  12381  reef11  12722  absefib  12801  efieq1re  12802  pc2dvds  13254  pcmpt  13263  subsubc  14052  odmulgid  15192  gexdvds  15220  submcmn2  15460  obslbs  16959  cnntr  17341  cndis  17357  cnindis  17358  cnpdis  17359  lmres  17366  cmpfi  17473  ist0-4  17763  txhmeo  17837  tsmssubm  18174  blin  18453  cncfmet  18940  icopnfcnv  18969  lmmbrf  19217  iscauf  19235  causs  19253  mbfposr  19546  itg2gt0  19654  limcflf  19770  limcres  19775  lhop1  19900  dvdsr1p  20086  fsumvma2  21000  vmasum  21002  chpchtsum  21005  bposlem1  21070  nbgraeledg  21444  nb3graprlem2  21463  cusgra3v  21475  cusgrauvtxb  21507  dmdmd  23805  funcnvmptOLD  24084  funcnvmpt  24085  xrdifh  24145  eqeelen  25845  leceifl  26242  iblabsnclem  26270  ftc1anclem6  26287  areacirclem5  26298  areacirc  26299  ellz1  26827  islssfg  27147  proot1ex  27499  el2spthonot0  28340  lsatfixedN  29809  cdlemg10c  31438  diaglbN  31855  dih1  32086  dihglbcpreN  32100  mapdcv  32460
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 179
  Copyright terms: Public domain W3C validator