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  1669  dfsbcq2  3007  unineq  3432  iindif2  3987  opeqex  4273  reusv2  4556  rabxfrd  4571  eqbrrdv  4800  eqbrrdiv  4801  opelco2g  4867  opelcnvg  4877  ralrnmpt  5685  fliftcnv  5826  ottpos  6260  eusvobj2  6353  smoiso  6395  ercnv  6697  ordiso2  7246  cantnfrescl  7394  cantnfp1lem3  7398  cantnflem1b  7404  cantnflem1  7407  cnfcom  7419  cnfcom3lem  7422  carden2  7636  cardeq0  8190  axpownd  8239  fpwwe2lem9  8276  fzen  10827  hasheq0  11369  incexc2  12313  divalglem4  12611  divalglem8  12615  divalgb  12619  divalgmod  12621  sadadd  12674  sadass  12678  smuval2  12689  smumul  12700  isprm3  12783  vdwmc  13041  imasleval  13459  acsfn2  13581  invsym2  13681  yoniso  14075  dprd2d2  15295  cmpfi  17151  xkoinjcn  17397  tgpconcomp  17811  iscau3  18720  mbfimaopnlem  19026  ellimc3  19245  eldv  19264  eltayl  19755  atandm3  20190  rmoxfrdOLD  23162  rmoxfrd  23163  ismbfm  23572  wl-bibi2d  24988  eqbrrdv2  26834  pmtrfmvdn0  27506  bnj1253  29363  islpln5  30346  islvol5  30390
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