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  2924  unineq  3326  iindif2  3869  opeqex  4150  reusv2  4431  rabxfrd  4446  eqbrrdv  4691  eqbrrdiv  4692  opelco2g  4758  opelcnvg  4768  ralrnmpt  5521  fliftcnv  5662  ottpos  6096  eusvobj2  6223  smoiso  6265  ercnv  6567  ordiso2  7114  cantnfrescl  7262  cantnfp1lem3  7266  cantnflem1b  7272  cantnflem1  7275  cnfcom  7287  cnfcom3lem  7290  carden2  7504  cardeq0  8056  axpownd  8103  fpwwe2lem9  8140  fzen  10689  hasheq0  11231  divalglem4  12469  divalglem8  12473  divalgb  12477  divalgmod  12479  sadadd  12532  sadass  12536  smuval2  12547  smumul  12558  isprm3  12641  vdwmc  12899  imasleval  13317  acsfn2  13409  invsym2  13509  yoniso  13903  dprd2d2  15114  cmpfi  16967  xkoinjcn  17213  tgpconcomp  17627  iscau3  18536  mbfimaopnlem  18842  ellimc3  19061  eldv  19080  eltayl  19571  atandm3  20006  wl-bibi2d  24090  eqbrrdv2  25897  pmtrfmvdn0  26569  bnj1253  27736  islpln5  28525  islvol5  28569
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