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

Theorem 3bitr3g 220
Description: More general version of 3bitr3i 208. 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 192 . 2 (𝜑 → (𝜃𝜒))
4 3bitr3g.3 . 2 (𝜒𝜏)
53, 4syl6bb 194 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:  con2bidc  803  sbal1yz  1920  sbal1  1921  dfsbcq2  2827  iindif2m  3765  opeqex  4032  rabxfrd  4247  eqbrrdv  4483  eqbrrdiv  4484  opelco2g  4551  opelcnvg  4563  ralrnmpt  5362  rexrnmpt  5363  fliftcnv  5487  eusvobj2  5550  f1od2  5908  ottposg  5925  ercnv  6215  djulf1o  6556  djurf1o  6557  fzen  9208  fihasheq0  9888  divalgb  10550  isprm3  10725
  Copyright terms: Public domain W3C validator