ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr3g Unicode 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  |-  ( 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, 2bitr3id 193 . 2  |-  ( ph  ->  ( th  <->  ch )
)
4 3bitr3g.3 . 2  |-  ( ch  <->  ta )
53, 4syl6bb 195 1  |-  ( ph  ->  ( th  <->  ta )
)
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  1977  sbal1  1978  dfsbcq2  2915  iindif2m  3886  opeqex  4177  rabxfrd  4396  eqbrrdv  4642  eqbrrdiv  4643  opelco2g  4713  opelcnvg  4725  ralrnmpt  5568  rexrnmpt  5569  fliftcnv  5702  eusvobj2  5766  f1od2  6138  ottposg  6158  ercnv  6456  exmidpw  6808  djuf1olem  6944  fzen  9852  fihasheq0  10570  divalgb  11651  isprm3  11828  eldvap  12852
  Copyright terms: Public domain W3C validator