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

Theorem 3bitr3g 220
Description: More general version of 3bitr3i 208. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.)
Hypotheses
Ref Expression
3bitr3g.1  |-  ( ph  ->  ( ps  <->  ch )
)
3bitr3g.2  |-  ( ps  <->  th )
3bitr3g.3  |-  ( ch  <->  ta )
Assertion
Ref Expression
3bitr3g  |-  ( ph  ->  ( th  <->  ta )
)

Proof of Theorem 3bitr3g
StepHypRef Expression
1 3bitr3g.2 . . 3  |-  ( ps  <->  th )
2 3bitr3g.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5bbr 192 . 2  |-  ( ph  ->  ( th  <->  ch )
)
4 3bitr3g.3 . 2  |-  ( ch  <->  ta )
53, 4syl6bb 194 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  con2bidc  805  sbal1yz  1922  sbal1  1923  dfsbcq2  2832  iindif2m  3782  opeqex  4052  rabxfrd  4267  eqbrrdv  4505  eqbrrdiv  4506  opelco2g  4574  opelcnvg  4586  ralrnmpt  5406  rexrnmpt  5407  fliftcnv  5537  eusvobj2  5601  f1od2  5959  ottposg  5976  ercnv  6267  exmidpw  6578  djuf1olem  6692  fzen  9392  fihasheq0  10120  divalgb  10850  isprm3  11025
  Copyright terms: Public domain W3C validator