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, 2bitr3id 193 . 2 (𝜑 → (𝜃𝜒))
4 3bitr3g.3 . 2 (𝜒𝜏)
53, 4bitrdi 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  861  sbal1yz  1981  sbal1  1982  dfsbcq2  2940  iindif2m  3916  opeqex  4209  rabxfrd  4428  eqbrrdv  4682  eqbrrdiv  4683  opelco2g  4753  opelcnvg  4765  ralrnmpt  5608  rexrnmpt  5609  fliftcnv  5742  eusvobj2  5807  f1od2  6179  ottposg  6199  ercnv  6498  exmidpw  6850  djuf1olem  6991  fzen  9938  fihasheq0  10661  divalgb  11808  isprm3  11986  eldvap  13022
 Copyright terms: Public domain W3C validator