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

Theorem 3imtr4g 262
Description: More general version of 3imtr4i 258. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
Hypotheses
Ref Expression
3imtr4g.1  |-  ( ph  ->  ( ps  ->  ch ) )
3imtr4g.2  |-  ( th  <->  ps )
3imtr4g.3  |-  ( ta  <->  ch )
Assertion
Ref Expression
3imtr4g  |-  ( ph  ->  ( th  ->  ta ) )

Proof of Theorem 3imtr4g
StepHypRef Expression
1 3imtr4g.2 . . 3  |-  ( th  <->  ps )
2 3imtr4g.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5bi 209 . 2  |-  ( ph  ->  ( th  ->  ch ) )
4 3imtr4g.3 . 2  |-  ( ta  <->  ch )
53, 4syl6ibr 219 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3anim123d  1261  3orim123d  1262  moim  2327  morimv  2329  2euswap  2357  ralim  2777  ralimdaa  2783  ralimdv2  2786  rexim  2810  reximdv2  2815  moeq3  3111  rmoim  3133  2reuswap  3136  ssel  3342  sstr2  3355  sscon  3481  ssdif  3482  unss1  3516  ssrin  3566  difin0ss  3694  r19.2z  3717  prel12  3975  uniss  4036  ssuni  4037  intss  4071  intssuni  4072  iunss1  4104  iinss1  4105  ss2iun  4108  disjss2  4185  disjss1  4188  disjss3  4211  ssbrd  4253  sspwb  4413  poss  4505  pofun  4519  soss  4521  frss  4549  sess1  4550  sess2  4551  wess  4569  reusv6OLD  4734  dfwe2  4762  onint  4775  orduniorsuc  4810  ordom  4854  finds  4871  finds2  4873  relss  4963  ssrel  4964  ssrel2  4966  ssrelrel  4976  xpsspw  4986  relop  5023  cnvss  5045  dmss  5069  dmcosseq  5137  funss  5472  fss  5599  fun  5607  brprcneu  5721  f1eqcocnv  6028  isores3  6055  isomin  6057  isopolem  6065  isosolem  6067  isowe2  6070  f1oweALT  6074  tposfn2  6501  tposfo2  6502  tposf1o2  6505  smores  6614  tz7.48lem  6698  tz7.48-3  6701  oaass  6804  iiner  6976  xpdom2  7203  ssenen  7281  pssnn  7327  hartogs  7513  card2on  7522  ackbij1  8118  cfub  8129  fin23lem27  8208  fin1a2lem11  8290  fin1a2lem13  8292  hsmexlem2  8307  zorn2lem4  8379  ondomon  8438  gchina  8574  intgru  8689  ingru  8690  addclprlem2  8894  psslinpr  8908  ltexprlem3  8915  ltexprlem4  8916  reclem2pr  8925  suplem1pr  8929  sup2  9964  nnind  10018  nnunb  10217  uzind  10361  xmullem2  10844  xrsupsslem  10885  xrinfmsslem  10886  seqof  11380  hashfacen  11703  sswrd  11737  wrdind  11791  cau3lem  12158  caubnd  12162  vdwnnlem2  13364  ramub2  13382  fthres2  14129  odupos  14562  lsmdisj2  15314  pgpfac1lem3  15635  subrgdvds  15882  lspdisj  16197  lspprat  16225  lbsextlem2  16231  ocv2ss  16900  ocvin  16901  tgcl  17034  epttop  17073  cmpsub  17463  tgcmp  17464  hauscmplem  17469  dfcon2  17482  llyss  17542  nllyss  17543  txcnpi  17640  txcnp  17652  snfil  17896  fgcl  17910  filcon  17915  filuni  17917  cfinfil  17925  csdfil  17926  supfil  17927  ufildom1  17958  fin1aufil  17964  fmfnfmlem3  17988  ptcmplem2  18084  cldsubg  18140  iscau3  19231  iscau4  19232  caussi  19250  volfiniun  19441  plycj  20195  abelth  20357  wilthlem2  20852  lgsdir2lem4  21110  pntleml  21305  cusgrafilem2  21489  lpni  21767  ubthlem1  22372  chintcli  22833  h1de2i  23055  spansnm0i  23152  strlem1  23753  mdslmd1i  23832  2reuswap2  23975  ssrmo  23981  rabss3d  23995  disjss1f  24016  disjpreima  24026  esumpcvgval  24468  derangenlem  24857  conpcon  24922  cvmsss2  24961  pocnv  25387  wzel  25575  sltres  25619  nocvxmin  25646  naim1  26134  naim2  26135  waj-ax  26164  lukshef-ax2  26165  itg2addnclem  26256  locfincmp  26384  ismtybndlem  26515  ablo4pnp  26555  isdrngo3  26575  keridl  26642  ispridl2  26648  ispridlc  26680  prter1  26728  mzpindd  26803  pellexlem3  26894  pellexlem5  26896  pellex  26898  2nn0ind  27008  lnr2i  27297  pm10.56  27542  ssrexf  27660  2rmoswap  27938  swrdccatin12lem3  28212  frisusgranb  28387  frgrancvvdeqlem3  28421  lshpdisj  29785  snatpsubN  30547  pmapglb2N  30568  pmapglb2xN  30569  elpaddn0  30597
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