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

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

Proof of Theorem 3bitr2d
StepHypRef Expression
1 3bitr2d.1 . . 3 (𝜑 → (𝜓𝜒))
2 3bitr2d.2 . . 3 (𝜑 → (𝜃𝜒))
31, 2bitr4d 184 . 2 (𝜑 → (𝜓𝜃))
4 3bitr2d.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitrd 181 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:  ceqsralt  2598  frecsuclem3  6021  indpi  6498  cauappcvgprlemladdru  6812  prsrlt  6929  lesub2  7526  ltsub2  7528  rec11ap  7761  avglt1  8220  rpnegap  8713  modqmuladdnn0  9318  expap0  9450  2shfti  9660  mulreap  9692  modremain  10241  nn0seqcvgd  10263
  Copyright terms: Public domain W3C validator