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  1700  dfsbcq2  3170  unineq  3576  iindif2  4184  opeqex  4476  reusv2  4758  rabxfrd  4773  eqbrrdv  5002  eqbrrdiv  5003  opelco2g  5069  opelcnvg  5081  ralrnmpt  5907  fliftcnv  6062  ottpos  6518  eusvobj2  6611  smoiso  6653  ercnv  6955  ordiso2  7513  cantnfrescl  7661  cantnfp1lem3  7665  cantnflem1b  7671  cantnflem1  7674  cnfcom  7686  cnfcom3lem  7689  carden2  7905  cardeq0  8458  axpownd  8507  fpwwe2lem9  8544  fzen  11103  hasheq0  11675  incexc2  12649  divalglem4  12947  divalglem8  12951  divalgb  12955  divalgmod  12957  sadadd  13010  sadass  13014  smuval2  13025  smumul  13036  isprm3  13119  vdwmc  13377  imasleval  13797  acsfn2  13919  invsym2  14019  yoniso  14413  dprd2d2  15633  cmpfi  17502  xkoinjcn  17750  tgpconcomp  18173  iscau3  19262  mbfimaopnlem  19576  ellimc3  19797  eldv  19816  eltayl  20307  atandm3  20749  rmoxfrdOLD  24010  rmoxfrd  24011  2ndpreima  24127  wl-bibi2d  26257  eqbrrdv2  26750  pmtrfmvdn0  27418  el2wlkonot  28425  el2spthonot  28426  bnj1253  29484  islpln5  30430  islvol5  30474
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