ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr4rd Unicode version

Theorem 3bitr4rd 220
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 190 . 2  |-  ( ph  ->  ( ta  <->  ps )
)
4 3bitr4d.2 . 2  |-  ( ph  ->  ( th  <->  ps )
)
53, 4bitr4d 190 1  |-  ( ph  ->  ( ta  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  inimasn  5018  dmfco  5551  omp1eomlem  7053  ltanqg  7335  genpassl  7459  genpassu  7460  ltexprlemloc  7542  caucvgprlemcanl  7579  cauappcvgprlemladdrl  7592  caucvgprlemladdrl  7613  caucvgprprlemaddq  7643  apneg  8503  lemuldiv  8770  msq11  8791  negiso  8844  avglt2  9090  xleaddadd  9817  iooshf  9882  qtri3or  10172  sq11ap  10616  hashen  10691  fihashdom  10710  cjap  10842  sqrt11ap  10974  mingeb  11177  xrnegiso  11197  clim2c  11219  climabs0  11242  absefib  11705  efieq1re  11706  nndivides  11731  oddnn02np1  11811  oddge22np1  11812  evennn02n  11813  evennn2n  11814  halfleoddlt  11825  pc2dvds  12255  pcmpt  12267  cnntr  12823  cndis  12839  cnpdis  12840  lmres  12846  txhmeo  12917  blininf  13022  cncfmet  13177
  Copyright terms: Public domain W3C validator