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  1693  dfsbcq2  3107  unineq  3534  iindif2  4101  opeqex  4388  reusv2  4669  rabxfrd  4684  eqbrrdv  4913  eqbrrdiv  4914  opelco2g  4980  opelcnvg  4992  ralrnmpt  5817  fliftcnv  5972  ottpos  6425  eusvobj2  6518  smoiso  6560  ercnv  6862  ordiso2  7417  cantnfrescl  7565  cantnfp1lem3  7569  cantnflem1b  7575  cantnflem1  7578  cnfcom  7590  cnfcom3lem  7593  carden2  7807  cardeq0  8360  axpownd  8409  fpwwe2lem9  8446  fzen  11004  hasheq0  11571  incexc2  12545  divalglem4  12843  divalglem8  12847  divalgb  12851  divalgmod  12853  sadadd  12906  sadass  12910  smuval2  12921  smumul  12932  isprm3  13015  vdwmc  13273  imasleval  13693  acsfn2  13815  invsym2  13915  yoniso  14309  dprd2d2  15529  cmpfi  17393  xkoinjcn  17640  tgpconcomp  18063  iscau3  19102  mbfimaopnlem  19414  ellimc3  19633  eldv  19652  eltayl  20143  atandm3  20585  rmoxfrdOLD  23823  rmoxfrd  23824  2ndpreima  23937  wl-bibi2d  25940  eqbrrdv2  26403  pmtrfmvdn0  27072  bnj1253  28724  islpln5  29649  islvol5  29693
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