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

Theorem 3bitr3g 278
Description: More general version of 3bitr3i 266. 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 250 . 2  |-  ( ph  ->  ( th  <->  ch )
)
4 3bitr3g.3 . 2  |-  ( ch  <->  ta )
53, 4syl6bb 252 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  notbid  285  cador  1396  equequ2  1691  dfsbcq2  3080  unineq  3507  iindif2  4073  opeqex  4360  reusv2  4643  rabxfrd  4658  eqbrrdv  4887  eqbrrdiv  4888  opelco2g  4954  opelcnvg  4964  ralrnmpt  5780  fliftcnv  5933  ottpos  6386  eusvobj2  6479  smoiso  6521  ercnv  6823  ordiso2  7377  cantnfrescl  7525  cantnfp1lem3  7529  cantnflem1b  7535  cantnflem1  7538  cnfcom  7550  cnfcom3lem  7553  carden2  7767  cardeq0  8321  axpownd  8370  fpwwe2lem9  8407  fzen  10964  hasheq0  11531  incexc2  12505  divalglem4  12803  divalglem8  12807  divalgb  12811  divalgmod  12813  sadadd  12866  sadass  12870  smuval2  12881  smumul  12892  isprm3  12975  vdwmc  13233  imasleval  13653  acsfn2  13775  invsym2  13875  yoniso  14269  dprd2d2  15489  cmpfi  17352  xkoinjcn  17598  tgpconcomp  18008  iscau3  18919  mbfimaopnlem  19225  ellimc3  19444  eldv  19463  eltayl  19954  atandm3  20396  rmoxfrdOLD  23494  rmoxfrd  23495  wl-bibi2d  25743  eqbrrdv2  26322  pmtrfmvdn0  26994  bnj1253  28799  islpln5  29783  islvol5  29827
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 177
  Copyright terms: Public domain W3C validator