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  1383  equequ2  1650  dfsbcq2  2995  unineq  3420  iindif2  3972  opeqex  4256  reusv2  4539  rabxfrd  4554  eqbrrdv  4783  eqbrrdiv  4784  opelco2g  4850  opelcnvg  4860  ralrnmpt  5630  fliftcnv  5771  ottpos  6205  eusvobj2  6332  smoiso  6374  ercnv  6676  ordiso2  7225  cantnfrescl  7373  cantnfp1lem3  7377  cantnflem1b  7383  cantnflem1  7386  cnfcom  7398  cnfcom3lem  7401  carden2  7615  cardeq0  8169  axpownd  8218  fpwwe2lem9  8255  fzen  10805  hasheq0  11347  incexc2  12291  divalglem4  12589  divalglem8  12593  divalgb  12597  divalgmod  12599  sadadd  12652  sadass  12656  smuval2  12667  smumul  12678  isprm3  12761  vdwmc  13019  imasleval  13437  acsfn2  13559  invsym2  13659  yoniso  14053  dprd2d2  15273  cmpfi  17129  xkoinjcn  17375  tgpconcomp  17789  iscau3  18698  mbfimaopnlem  19004  ellimc3  19223  eldv  19242  eltayl  19733  atandm3  20168  wl-bibi2d  24323  eqbrrdv2  26130  pmtrfmvdn0  26802  bnj1253  28314  islpln5  28991  islvol5  29035
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