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

Theorem 3bitr3g 279
Description: More general version of 3bitr3i 267. 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 251 . 2  |-  ( ph  ->  ( th  <->  ch )
)
4 3bitr3g.3 . 2  |-  ( ch  <->  ta )
53, 4syl6bb 253 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  notbid  286  cador  1400  equequ2  1698  dfsbcq2  3151  unineq  3578  iindif2  4147  opeqex  4434  reusv2  4715  rabxfrd  4730  eqbrrdv  4959  eqbrrdiv  4960  opelco2g  5026  opelcnvg  5038  ralrnmpt  5864  fliftcnv  6019  ottpos  6475  eusvobj2  6568  smoiso  6610  ercnv  6912  ordiso2  7468  cantnfrescl  7616  cantnfp1lem3  7620  cantnflem1b  7626  cantnflem1  7629  cnfcom  7641  cnfcom3lem  7644  carden2  7858  cardeq0  8411  axpownd  8460  fpwwe2lem9  8497  fzen  11056  hasheq0  11627  incexc2  12601  divalglem4  12899  divalglem8  12903  divalgb  12907  divalgmod  12909  sadadd  12962  sadass  12966  smuval2  12977  smumul  12988  isprm3  13071  vdwmc  13329  imasleval  13749  acsfn2  13871  invsym2  13971  yoniso  14365  dprd2d2  15585  cmpfi  17454  xkoinjcn  17702  tgpconcomp  18125  iscau3  19214  mbfimaopnlem  19530  ellimc3  19749  eldv  19768  eltayl  20259  atandm3  20701  rmoxfrdOLD  23962  rmoxfrd  23963  2ndpreima  24079  wl-bibi2d  26169  eqbrrdv2  26644  pmtrfmvdn0  27313  el2wlkonot  28108  el2spthonot  28109  bnj1253  29138  islpln5  30063  islvol5  30107
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 178
  Copyright terms: Public domain W3C validator