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  1381  equequ2  1649  dfsbcq2  2994  unineq  3419  iindif2  3971  opeqex  4257  reusv2  4540  rabxfrd  4555  eqbrrdv  4784  eqbrrdiv  4785  opelco2g  4851  opelcnvg  4861  ralrnmpt  5669  fliftcnv  5810  ottpos  6244  eusvobj2  6337  smoiso  6379  ercnv  6681  ordiso2  7230  cantnfrescl  7378  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1  7391  cnfcom  7403  cnfcom3lem  7406  carden2  7620  cardeq0  8174  axpownd  8223  fpwwe2lem9  8260  fzen  10811  hasheq0  11353  incexc2  12297  divalglem4  12595  divalglem8  12599  divalgb  12603  divalgmod  12605  sadadd  12658  sadass  12662  smuval2  12673  smumul  12684  isprm3  12767  vdwmc  13025  imasleval  13443  acsfn2  13565  invsym2  13665  yoniso  14059  dprd2d2  15279  cmpfi  17135  xkoinjcn  17381  tgpconcomp  17795  iscau3  18704  mbfimaopnlem  19010  ellimc3  19229  eldv  19248  eltayl  19739  atandm3  20174  wl-bibi2d  24327  eqbrrdv2  26143  pmtrfmvdn0  26815  bnj1253  28420  islpln5  29097  islvol5  29141
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