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  4956  dmfco  5489  omp1eomlem  6979  ltanqg  7215  genpassl  7339  genpassu  7340  ltexprlemloc  7422  caucvgprlemcanl  7459  cauappcvgprlemladdrl  7472  caucvgprlemladdrl  7493  caucvgprprlemaddq  7523  apneg  8380  lemuldiv  8646  msq11  8667  negiso  8720  avglt2  8966  xleaddadd  9677  iooshf  9742  qtri3or  10027  sq11ap  10465  hashen  10537  fihashdom  10556  cjap  10685  sqrt11ap  10817  xrnegiso  11038  clim2c  11060  climabs0  11083  absefib  11484  efieq1re  11485  nndivides  11507  oddnn02np1  11584  oddge22np1  11585  evennn02n  11586  evennn2n  11587  halfleoddlt  11598  cnntr  12404  cndis  12420  cnpdis  12421  lmres  12427  txhmeo  12498  blininf  12603  cncfmet  12758
  Copyright terms: Public domain W3C validator