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

Theorem 3imtr4g 270
Description: More general version of 3imtr4i 266. 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
3imtr4g.2
3imtr4g.3
Assertion
Ref Expression
3imtr4g

Proof of Theorem 3imtr4g
StepHypRef Expression
1 3imtr4g.2 . . 3
2 3imtr4g.1 . . 3
31, 2syl5bi 217 . 2
4 3imtr4g.3 . 2
53, 4syl6ibr 227 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  3anim123d  1306  3orim123d  1307  mo3  2323  mo3OLD  2324  moim  2339  morimvOLD  2342  2euswap  2370  nelcon3d  2806  ral2imi  2845  ralimOLD  2851  ralimdaaOLD  2860  ralimdv2  2864  rexim  2922  reximd2a  2927  reximdv2  2928  moeq3  3276  rmoim  3299  2reuswap  3302  ssel  3497  sstr2  3510  sscon  3637  ssdif  3638  unss1  3672  ssrin  3722  difin0ss  3894  r19.2z  3918  prel12  4207  uniss  4270  ssuni  4271  intssOLD  4308  intssuni  4309  iunss1  4342  iinss1  4343  ss2iun  4346  disjss2  4425  disjss1  4428  disjss3  4451  ssbrd  4493  reusv6OLD  4663  sspwb  4701  poss  4807  pofun  4821  soss  4823  frss  4851  sess1  4852  sess2  4853  wess  4871  relss  5095  ssrel  5096  ssrel2  5098  ssrelrel  5108  xpsspw  5121  relop  5158  cnvss  5180  dmss  5207  dmcosseq  5269  funss  5611  fss  5744  fun  5753  brprcneu  5864  f1eqcocnv  6204  isores3  6231  isomin  6233  isopolem  6241  isosolem  6243  isowe2  6246  ovmpt2s  6426  dfwe2  6617  onint  6630  orduniorsuc  6665  ordom  6709  finds  6726  finds2  6728  f1oweALT  6784  tposfn2  6996  tposfo2  6997  tposf1o2  7000  smores  7042  tz7.48lem  7125  tz7.48-3  7128  oaass  7229  iiner  7402  xpdom2  7632  ssenen  7711  pssnn  7758  hartogs  7990  card2on  8001  ackbij1  8639  cfub  8650  fin23lem27  8729  fin1a2lem11  8811  fin1a2lem13  8813  hsmexlem2  8828  zorn2lem4  8900  ondomon  8959  gchina  9098  intgru  9213  ingru  9214  addclprlem2  9416  psslinpr  9430  ltexprlem3  9437  ltexprlem4  9438  reclem2pr  9447  suplem1pr  9451  sup2  10524  nnind  10579  nnunb  10816  uzind  10979  xmullem2  11486  xrsupsslem  11527  xrinfmsslem  11528  seqof  12164  hashfacen  12503  sswrd  12555  wrdind  12702  wrd2ind  12703  swrdccatin12lem2  12714  cau3lem  13187  caubnd  13191  vdwnnlem2  14514  ramub2  14532  fthres2  15301  odupos  15765  lsmdisj2  16700  pgpfac1lem3  17128  subrgdvds  17443  lspdisj  17771  lspprat  17799  lbsextlem2  17805  coe1fzgsumd  18344  evl1gsumd  18393  ocv2ss  18704  ocvin  18705  tgcl  19471  epttop  19510  cmpsub  19900  tgcmp  19901  hauscmplem  19906  dfcon2  19920  llyss  19980  nllyss  19981  locfincmp  20027  txcnpi  20109  txcnp  20121  snfil  20365  fgcl  20379  filcon  20384  filuni  20386  cfinfil  20394  csdfil  20395  supfil  20396  ufildom1  20427  fin1aufil  20433  fmfnfmlem3  20457  ptcmplem2  20553  cldsubg  20609  iscau3  21717  iscau4  21718  caussi  21736  volfiniun  21957  plycj  22674  abelth  22836  wilthlem2  23343  lgsdir2lem4  23601  pntleml  23796  cusgrafilem2  24480  frisusgranb  24997  frgrancvvdeqlem3  25032  lpni  25181  ubthlem1  25786  chintcli  26249  h1de2i  26471  spansnm0i  26568  strlem1  27169  mdslmd1i  27248  2reuswap2  27387  ssrmo  27393  rabss3d  27412  disjss1f  27435  disjpreima  27445  ssrelf  27466  suppss3  27550  nnindf  27610  oduprs  27644  crefss  27852  esumpcvgval  28084  derangenlem  28615  conpcon  28680  cvmsss2  28719  pocnv  29193  wzel  29380  sltres  29424  nocvxmin  29451  naim1  29850  naim2  29851  waj-ax  29879  lukshef-ax2  29880  itg2addnclem  30066  ismtybndlem  30302  ablo4pnp  30342  isdrngo3  30362  keridl  30429  ispridl2  30435  ispridlc  30467  prter1  30620  mzpindd  30678  pellexlem3  30767  pellexlem5  30769  pellex  30771  2nn0ind  30881  lnr2i  31065  ssrexf  31388  2rmoswap  32189  nrhmzr  32679  lshpdisj  34712  snatpsubN  35474  pmapglb2N  35495  pmapglb2xN  35496  elpaddn0  35524  hess  37803  frege52aid  37885  frege52b  37916
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 185
  Copyright terms: Public domain W3C validator