ILE Home 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  762  sbal1yz  1859  sbal1  1860  dfsbcq2  2744  iindif2m  3698  opeqex  3960  rabxfrd  4151  eqbrrdv  4364  eqbrrdiv  4365  opelco2g  4430  opelcnvg  4442  ralrnmpt  5234  rexrnmpt  5235  fliftcnv  5360  eusvobj2  5422  ottposg  5792  ercnv  6038
  Copyright terms: Public domain W3C validator