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  876  sbal1yz  2013  sbal1  2014  dfsbcq2  2980  iindif2m  3969  opeqex  4267  rabxfrd  4487  eqbrrdv  4741  eqbrrdiv  4742  opelco2g  4813  opelcnvg  4825  ralrnmpt  5679  rexrnmpt  5680  fliftcnv  5817  eusvobj2  5883  f1od2  6261  ottposg  6281  ercnv  6581  exmidpw  6937  djuf1olem  7083  fzen  10075  fihasheq0  10808  divalgb  11965  isprm3  12153  eldvap  14628
  Copyright terms: Public domain W3C validator