ILE Home 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  2739  frecsuclem  6353  indpi  7262  cauappcvgprlemladdru  7576  prsrlt  7707  lesub2  8332  ltsub2  8334  rec11ap  8583  avglt1  9071  rpnegap  9593  modqmuladdnn0  10267  expap0  10449  2shfti  10731  mulreap  10764  minmax  11129  lemininf  11133  xrminmax  11162  xrlemininf  11168  modremain  11819  nn0seqcvgd  11917  divgcdcoprm0  11977  isxmet2d  12748  xblss2  12805  neibl  12891  ellimc3apf  13029  logbgt0b  13283  iswomninnlem  13620
  Copyright terms: Public domain W3C validator