MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitr3g Unicode version

Theorem 3bitr3g 279
Description: More general version of 3bitr3i 267. 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 251 . 2  |-  ( ph  ->  ( th  <->  ch )
)
4 3bitr3g.3 . 2  |-  ( ch  <->  ta )
53, 4syl6bb 253 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  notbid  286  cador  1397  equequ2  1694  dfsbcq2  3128  unineq  3555  iindif2  4124  opeqex  4411  reusv2  4692  rabxfrd  4707  eqbrrdv  4936  eqbrrdiv  4937  opelco2g  5003  opelcnvg  5015  ralrnmpt  5841  fliftcnv  5996  ottpos  6452  eusvobj2  6545  smoiso  6587  ercnv  6889  ordiso2  7444  cantnfrescl  7592  cantnfp1lem3  7596  cantnflem1b  7602  cantnflem1  7605  cnfcom  7617  cnfcom3lem  7620  carden2  7834  cardeq0  8387  axpownd  8436  fpwwe2lem9  8473  fzen  11032  hasheq0  11603  incexc2  12577  divalglem4  12875  divalglem8  12879  divalgb  12883  divalgmod  12885  sadadd  12938  sadass  12942  smuval2  12953  smumul  12964  isprm3  13047  vdwmc  13305  imasleval  13725  acsfn2  13847  invsym2  13947  yoniso  14341  dprd2d2  15561  cmpfi  17429  xkoinjcn  17676  tgpconcomp  18099  iscau3  19188  mbfimaopnlem  19504  ellimc3  19723  eldv  19742  eltayl  20233  atandm3  20675  rmoxfrdOLD  23936  rmoxfrd  23937  2ndpreima  24053  wl-bibi2d  26134  eqbrrdv2  26606  pmtrfmvdn0  27275  el2wlkonot  28070  el2spthonot  28071  bnj1253  29096  islpln5  30021  islvol5  30065
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator