MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitr3g Structured version   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 4    <-> wb 178
This theorem is referenced by:  notbid  287  cador  1401  equequ2  1699  dfsbcq2  3166  unineq  3593  iindif2  4162  opeqex  4450  reusv2  4732  rabxfrd  4747  eqbrrdv  4976  eqbrrdiv  4977  opelco2g  5043  opelcnvg  5055  ralrnmpt  5881  fliftcnv  6036  ottpos  6492  eusvobj2  6585  smoiso  6627  ercnv  6929  ordiso2  7487  cantnfrescl  7635  cantnfp1lem3  7639  cantnflem1b  7645  cantnflem1  7648  cnfcom  7660  cnfcom3lem  7663  carden2  7879  cardeq0  8432  axpownd  8481  fpwwe2lem9  8518  fzen  11077  hasheq0  11649  incexc2  12623  divalglem4  12921  divalglem8  12925  divalgb  12929  divalgmod  12931  sadadd  12984  sadass  12988  smuval2  12999  smumul  13010  isprm3  13093  vdwmc  13351  imasleval  13771  acsfn2  13893  invsym2  13993  yoniso  14387  dprd2d2  15607  cmpfi  17476  xkoinjcn  17724  tgpconcomp  18147  iscau3  19236  mbfimaopnlem  19550  ellimc3  19771  eldv  19790  eltayl  20281  atandm3  20723  rmoxfrdOLD  23984  rmoxfrd  23985  2ndpreima  24101  wl-bibi2d  26231  eqbrrdv2  26726  pmtrfmvdn0  27394  el2wlkonot  28401  el2spthonot  28402  bnj1253  29460  islpln5  30406  islvol5  30450
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator