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

Theorem 3bitr3d 217
Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.)
Hypotheses
Ref Expression
3bitr3d.1 (𝜑 → (𝜓𝜒))
3bitr3d.2 (𝜑 → (𝜓𝜃))
3bitr3d.3 (𝜑 → (𝜒𝜏))
Assertion
Ref Expression
3bitr3d (𝜑 → (𝜃𝜏))

Proof of Theorem 3bitr3d
StepHypRef Expression
1 3bitr3d.2 . . 3 (𝜑 → (𝜓𝜃))
2 3bitr3d.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2bitr3d 189 . 2 (𝜑 → (𝜃𝜒))
4 3bitr3d.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:  csbcomg  3029  eloprabga  5865  ereldm  6479  mapen  6747  ordiso2  6927  subcan  8040  conjmulap  8512  ltrec  8664  divelunit  9814  fseq1m1p1  9905  fzm1  9910  fihashneq0  10572  hashfacen  10610  cvg1nlemcau  10787  lenegsq  10898  dvdsmod  11594  bezoutlemle  11730  rpexp  11865  qnumdenbi  11904  bdxmet  12707  txmetcnp  12724  cnmet  12736
  Copyright terms: Public domain W3C validator