Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr3g 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  769  sbal1yz  1877  sbal1  1878  dfsbcq2  2767  iindif2m  3724  opeqex  3986  rabxfrd  4201  eqbrrdv  4437  eqbrrdiv  4438  opelco2g  4503  opelcnvg  4515  ralrnmpt  5309  rexrnmpt  5310  fliftcnv  5435  eusvobj2  5498  ottposg  5870  ercnv  6127  fzen  8907
 Copyright terms: Public domain W3C validator