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  2955  unineq  3380  iindif2  3931  opeqex  4215  reusv2  4498  rabxfrd  4513  eqbrrdv  4758  eqbrrdiv  4759  opelco2g  4825  opelcnvg  4835  ralrnmpt  5589  fliftcnv  5730  ottpos  6164  eusvobj2  6291  smoiso  6333  ercnv  6635  ordiso2  7184  cantnfrescl  7332  cantnfp1lem3  7336  cantnflem1b  7342  cantnflem1  7345  cnfcom  7357  cnfcom3lem  7360  carden2  7574  cardeq0  8128  axpownd  8177  fpwwe2lem9  8214  fzen  10763  hasheq0  11305  divalglem4  12543  divalglem8  12547  divalgb  12551  divalgmod  12553  sadadd  12606  sadass  12610  smuval2  12621  smumul  12632  isprm3  12715  vdwmc  12973  imasleval  13391  acsfn2  13513  invsym2  13613  yoniso  14007  dprd2d2  15227  cmpfi  17083  xkoinjcn  17329  tgpconcomp  17743  iscau3  18652  mbfimaopnlem  18958  ellimc3  19177  eldv  19196  eltayl  19687  atandm3  20122  wl-bibi2d  24277  eqbrrdv2  26084  pmtrfmvdn0  26756  bnj1253  28080  islpln5  28875  islvol5  28919
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