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

Theorem 3bitr3g 280
Description: More general version of 3bitr3i 268. 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 252 . 2  |-  ( ph  ->  ( th  <->  ch )
)
4 3bitr3g.3 . 2  |-  ( ch  <->  ta )
53, 4syl6bb 254 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178
This theorem is referenced by:  notbid  287  cador  1387  dfsbcq2  2938  unineq  3361  iindif2  3912  opeqex  4194  reusv2  4477  rabxfrd  4492  eqbrrdv  4737  eqbrrdiv  4738  opelco2g  4804  opelcnvg  4814  ralrnmpt  5568  fliftcnv  5709  ottpos  6143  eusvobj2  6270  smoiso  6312  ercnv  6614  ordiso2  7163  cantnfrescl  7311  cantnfp1lem3  7315  cantnflem1b  7321  cantnflem1  7324  cnfcom  7336  cnfcom3lem  7339  carden2  7553  cardeq0  8107  axpownd  8156  fpwwe2lem9  8193  fzen  10742  hasheq0  11284  divalglem4  12522  divalglem8  12526  divalgb  12530  divalgmod  12532  sadadd  12585  sadass  12589  smuval2  12600  smumul  12611  isprm3  12694  vdwmc  12952  imasleval  13370  acsfn2  13492  invsym2  13592  yoniso  13986  dprd2d2  15206  cmpfi  17062  xkoinjcn  17308  tgpconcomp  17722  iscau3  18631  mbfimaopnlem  18937  ellimc3  19156  eldv  19175  eltayl  19666  atandm3  20101  wl-bibi2d  24256  eqbrrdv2  26063  pmtrfmvdn0  26735  bnj1253  28059  islpln5  28854  islvol5  28898
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator