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

Theorem 3bitr3g 222
Description: More general version of 3bitr3i 210. 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, 2bitr3id 194 . 2 (𝜑 → (𝜃𝜒))
4 3bitr3g.3 . 2 (𝜒𝜏)
53, 4bitrdi 196 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  con2bidc  875  sbal1yz  2001  sbal1  2002  dfsbcq2  2966  iindif2m  3955  opeqex  4250  rabxfrd  4470  eqbrrdv  4724  eqbrrdiv  4725  opelco2g  4796  opelcnvg  4808  ralrnmpt  5659  rexrnmpt  5660  fliftcnv  5796  eusvobj2  5861  f1od2  6236  ottposg  6256  ercnv  6556  exmidpw  6908  djuf1olem  7052  fzen  10043  fihasheq0  10773  divalgb  11930  isprm3  12118  eldvap  14154
  Copyright terms: Public domain W3C validator