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

Theorem 3bitr3g 221
Description: More general version of 3bitr3i 209. 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 193 . 2 (𝜑 → (𝜃𝜒))
4 3bitr3g.3 . 2 (𝜒𝜏)
53, 4syl6bb 195 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  con2bidc  843  sbal1yz  1952  sbal1  1953  dfsbcq2  2883  iindif2m  3848  opeqex  4139  rabxfrd  4358  eqbrrdv  4604  eqbrrdiv  4605  opelco2g  4675  opelcnvg  4687  ralrnmpt  5528  rexrnmpt  5529  fliftcnv  5662  eusvobj2  5726  f1od2  6098  ottposg  6118  ercnv  6416  exmidpw  6768  djuf1olem  6904  fzen  9774  fihasheq0  10491  divalgb  11529  isprm3  11706  eldvap  12726
  Copyright terms: Public domain W3C validator