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

Theorem 3bitr4rd 214
 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 184 . 2 (𝜑 → (𝜏𝜓))
4 3bitr4d.2 . 2 (𝜑 → (𝜃𝜓))
53, 4bitr4d 184 1 (𝜑 → (𝜏𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  inimasn  4768  dmfco  5268  ltanqg  6555  genpassl  6679  genpassu  6680  ltexprlemloc  6762  caucvgprlemcanl  6799  cauappcvgprlemladdrl  6812  caucvgprlemladdrl  6833  caucvgprprlemaddq  6863  apneg  7675  lemuldiv  7921  msq11  7942  avglt2  8220  iooshf  8921  qtri3or  9199  sq11ap  9576  cjap  9727  sqrt11ap  9857  clim2c  10028  climabs0  10051  nndivides  10107  oddnn02np1  10184  oddge22np1  10185  evennn02n  10186  evennn2n  10187  halfleoddlt  10198
 Copyright terms: Public domain W3C validator