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

Theorem 3imtr4g 285
Description: More general version of 3imtr4i 281. 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 232 . 2 (𝜑 → (𝜃𝜒))
4 3imtr4g.3 . 2 (𝜏𝜒)
53, 4syl6ibr 242 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  3anim123d  1446  3orim123d  1447  mo3  2536  moim  2548  2euswap  2577  nelcon3d  2938  ral2imi  2976  ralimdv2  2990  rexim  3037  reximd2a  3042  reximdv2  3043  moeq3  3416  rmoim  3440  2reuswap  3443  ssel  3630  sstr2  3643  ssrexf  3698  sscon  3777  ssdif  3778  unss1  3815  ssrin  3871  difin0ss  3979  r19.2z  4093  prel12  4414  uniss  4490  ssuni  4491  ssuniOLD  4492  intssuni  4531  iunss1  4564  iinss1  4565  ss2iun  4568  iunxdif3  4638  disjss2  4655  disjss1  4658  disjss3  4684  ssbrd  4728  sspwb  4947  poss  5066  pofun  5080  soss  5082  frss  5110  sess1  5111  sess2  5112  wess  5130  relss  5240  ssrelOLD  5242  ssrel2  5244  ssrelrel  5254  relop  5305  dmss  5355  dmcosseq  5419  funss  5945  fss  6094  fun  6104  brprcneu  6222  f1eqcocnv  6596  isores3  6625  isomin  6627  isopolem  6635  isosolem  6637  isowe2  6640  ovmpt2s  6826  dfwe2  7023  onint  7037  orduniorsuc  7072  ordom  7116  finds  7134  finds2  7136  f1oweALT  7194  tposfn2  7419  tposfo2  7420  tposf1o2  7423  smores  7494  tz7.48lem  7581  tz7.48-3  7584  oaass  7686  iiner  7862  xpdom2  8096  ssenen  8175  pssnn  8219  hartogs  8490  card2on  8500  ackbij1  9098  cfub  9109  fin23lem27  9188  fin1a2lem11  9270  fin1a2lem13  9272  hsmexlem2  9287  zorn2lem4  9359  ondomon  9423  gchina  9559  intgru  9674  ingru  9675  addclprlem2  9877  psslinpr  9891  ltexprlem3  9898  ltexprlem4  9899  reclem2pr  9908  suplem1pr  9912  sup2  11017  nnind  11076  nnunb  11326  uzind  11507  xmullem2  12133  xrsupsslem  12175  xrinfmsslem  12176  seqof  12898  hashfacen  13276  sswrd  13345  wrdind  13522  wrd2ind  13523  swrdccatin12lem2  13535  cau3lem  14138  caubnd  14142  sumodd  15158  vdwnnlem2  15747  ramub2  15765  setsstructOLD  15946  fthres2  16639  odupos  17182  lsmdisj2  18141  pgpfac1lem3  18522  subrgdvds  18842  lspdisj  19173  lspprat  19201  lbsextlem2  19207  coe1fzgsumd  19720  evl1gsumd  19769  ocv2ss  20065  ocvin  20066  tgcl  20821  epttop  20861  cmpsub  21251  tgcmp  21252  hauscmplem  21257  dfconn2  21270  llyss  21330  nllyss  21331  locfincmp  21377  txcnpi  21459  txcnp  21471  snfil  21715  fgcl  21729  filconn  21734  filuni  21736  cfinfil  21744  csdfil  21745  supfil  21746  ufildom1  21777  fin1aufil  21783  fmfnfmlem3  21807  ptcmplem2  21904  cldsubg  21961  iscau3  23122  iscau4  23123  caussi  23141  volfiniun  23361  plycj  24078  abelth  24240  wilthlem2  24840  lgsdir2lem4  25098  gausslemma2dlem0i  25134  gausslemma2dlem1a  25135  pntleml  25345  uhgr0vsize0  26176  cusgrfilem2  26408  uhgrvd00  26486  clwwisshclwws  26972  frcond3  27249  frgrncvvdeqlem2  27280  lpni  27462  ubthlem1  27854  chintcli  28318  h1de2i  28540  spansnm0i  28637  strlem1  29237  mdslmd1i  29316  2reuswap2  29455  ssrmo  29461  rabss3d  29477  iinssiun  29503  disjss1f  29512  disjpreima  29523  ssrelf  29553  suppss3  29630  nnindf  29693  oduprs  29784  crefss  30044  esumpcvgval  30268  derangenlem  31279  connpconn  31343  cvmsss2  31382  pocnv  31779  wzel  31894  sltres  31940  nosupno  31974  nocvxmin  32019  naim1  32509  naim2  32510  waj-ax  32538  lukshef-ax2  32539  bj-ssbim  32746  bj-mo3OLD  32957  poimirlem26  33565  poimirlem30  33569  poimirlem32  33571  itg2addnclem  33591  ismtybndlem  33735  ablo4pnp  33809  isdrngo3  33888  keridl  33961  ispridl2  33967  ispridlc  33999  trcoss  34372  prter1  34483  lshpdisj  34592  snatpsubN  35354  pmapglb2N  35375  pmapglb2xN  35376  elpaddn0  35404  mzpindd  37626  pellexlem3  37712  pellexlem5  37714  pellex  37716  2nn0ind  37827  lnr2i  38003  intabssd  38233  iunrelexpuztr  38328  hess  38391  frege52aid  38469  frege52b  38500  neik0pk1imk0  38662  2rmoswap  41505  pfxccatin12lem2  41749  nrhmzr  42198  elsetrecslem  42770
  Copyright terms: Public domain W3C validator