ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr3g Structured version   Unicode 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  768  sbal1yz  1874  sbal1  1875  dfsbcq2  2761  iindif2m  3715  opeqex  3977  rabxfrd  4167  eqbrrdv  4380  eqbrrdiv  4381  opelco2g  4446  opelcnvg  4458  ralrnmpt  5252  rexrnmpt  5253  fliftcnv  5378  eusvobj2  5441  ottposg  5811  ercnv  6063  fzen  8637
  Copyright terms: Public domain W3C validator