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

Theorem 3bitr3d 216
 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 188 . 2 (𝜑 → (𝜃𝜒))
4 3bitr3d.3 . 2 (𝜑 → (𝜒𝜏))
53, 4bitrd 186 1 (𝜑 → (𝜃𝜏))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 103 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106 This theorem depends on definitions:  df-bi 115 This theorem is referenced by:  csbcomg  2930  eloprabga  5622  ereldm  6215  ordiso2  6505  subcan  7430  conjmulap  7884  ltrec  8028  divelunit  9100  fseq1m1p1  9188  fzm1  9193  sizeneq0  9819  cvg1nlemcau  10008  lenegsq  10119  dvdsmod  10407  bezoutlemle  10541  rpexp  10676
 Copyright terms: Public domain W3C validator