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

Theorem 3bitr4rd 219
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr4d.1 (𝜑 → (𝜓𝜒))
3bitr4d.2 (𝜑 → (𝜃𝜓))
3bitr4d.3 (𝜑 → (𝜏𝜒))
Assertion
Ref Expression
3bitr4rd (𝜑 → (𝜏𝜃))

Proof of Theorem 3bitr4rd
StepHypRef Expression
1 3bitr4d.3 . . 3 (𝜑 → (𝜏𝜒))
2 3bitr4d.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2bitr4d 189 . 2 (𝜑 → (𝜏𝜓))
4 3bitr4d.2 . 2 (𝜑 → (𝜃𝜓))
53, 4bitr4d 189 1 (𝜑 → (𝜏𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  inimasn  4817  dmfco  5337  ltanqg  6906  genpassl  7030  genpassu  7031  ltexprlemloc  7113  caucvgprlemcanl  7150  cauappcvgprlemladdrl  7163  caucvgprlemladdrl  7184  caucvgprprlemaddq  7214  apneg  8032  lemuldiv  8280  msq11  8301  negiso  8354  avglt2  8591  iooshf  9305  qtri3or  9585  sq11ap  10038  hashen  10110  fihashdom  10129  cjap  10257  sqrt11ap  10388  clim2c  10588  climabs0  10612  nndivides  10728  oddnn02np1  10805  oddge22np1  10806  evennn02n  10807  evennn2n  10808  halfleoddlt  10819
  Copyright terms: Public domain W3C validator