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  4926  dmfco  5457  omp1eomlem  6947  ltanqg  7176  genpassl  7300  genpassu  7301  ltexprlemloc  7383  caucvgprlemcanl  7420  cauappcvgprlemladdrl  7433  caucvgprlemladdrl  7454  caucvgprprlemaddq  7484  apneg  8340  lemuldiv  8603  msq11  8624  negiso  8677  avglt2  8917  xleaddadd  9625  iooshf  9690  qtri3or  9975  sq11ap  10413  hashen  10485  fihashdom  10504  cjap  10633  sqrt11ap  10765  xrnegiso  10986  clim2c  11008  climabs0  11031  absefib  11391  efieq1re  11392  nndivides  11412  oddnn02np1  11489  oddge22np1  11490  evennn02n  11491  evennn2n  11492  halfleoddlt  11503  cnntr  12305  cndis  12321  cnpdis  12322  lmres  12328  txhmeo  12399  blininf  12504  cncfmet  12659
  Copyright terms: Public domain W3C validator