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

Theorem 3bitr4rd 210
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 180 . 2 (φ → (τψ))
4 3bitr4d.2 . 2 (φ → (θψ))
53, 4bitr4d 180 1 (φ → (τθ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  inimasn  4684  dmfco  5184  ltanqg  6384  genpassl  6507  genpassu  6508  ltexprlemloc  6581  cauappcvgprlemcan  6616  cauappcvgprlemladdrl  6629  caucvgprlemladdrl  6649  apneg  7395  lemuldiv  7628  msq11  7649  avglt2  7941  iooshf  8591  cjap  9134
  Copyright terms: Public domain W3C validator