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

Theorem 3bitr3g 211
 Description: More general version of 3bitr3i 199. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.)
Hypotheses
Ref Expression
3bitr3g.1 (φ → (ψχ))
3bitr3g.2 (ψθ)
3bitr3g.3 (χτ)
Assertion
Ref Expression
3bitr3g (φ → (θτ))

Proof of Theorem 3bitr3g
StepHypRef Expression
1 3bitr3g.2 . . 3 (ψθ)
2 3bitr3g.1 . . 3 (φ → (ψχ))
31, 2syl5bbr 183 . 2 (φ → (θχ))
4 3bitr3g.3 . 2 (χτ)
53, 4syl6bb 185 1 (φ → (θτ))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  con2bidc  768  sbal1yz  1874  sbal1  1875  dfsbcq2  2761  iindif2m  3715  opeqex  3977  rabxfrd  4167  eqbrrdv  4380  eqbrrdiv  4381  opelco2g  4446  opelcnvg  4458  ralrnmpt  5252  rexrnmpt  5253  fliftcnv  5378  eusvobj2  5441  ottposg  5811  ercnv  6063  fzen  8657
 Copyright terms: Public domain W3C validator