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

Theorem 3bitr2d 215
 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 190 . 2 (𝜑 → (𝜓𝜃))
4 3bitr2d.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitrd 187 1 (𝜑 → (𝜓𝜏))
 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:  ceqsralt  2713  frecsuclem  6303  indpi  7150  cauappcvgprlemladdru  7464  prsrlt  7595  lesub2  8219  ltsub2  8221  rec11ap  8470  avglt1  8958  rpnegap  9474  modqmuladdnn0  10141  expap0  10323  2shfti  10603  mulreap  10636  minmax  11001  lemininf  11005  xrminmax  11034  xrlemininf  11040  modremain  11626  nn0seqcvgd  11722  divgcdcoprm0  11782  isxmet2d  12517  xblss2  12574  neibl  12660  ellimc3apf  12798
 Copyright terms: Public domain W3C validator