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  805  sbal1yz  1922  sbal1  1923  dfsbcq2  2832  iindif2m  3780  opeqex  4050  rabxfrd  4265  eqbrrdv  4503  eqbrrdiv  4504  opelco2g  4572  opelcnvg  4584  ralrnmpt  5404  rexrnmpt  5405  fliftcnv  5535  eusvobj2  5599  f1od2  5957  ottposg  5974  ercnv  6265  exmidpw  6576  djuf1olem  6689  fzen  9389  fihasheq0  10098  divalgb  10800  isprm3  10975
  Copyright terms: Public domain W3C validator