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

Theorem 3imtr4g 283
Description: More general version of 3imtr4i 279. 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 230 . 2 (𝜑 → (𝜃𝜒))
4 3imtr4g.3 . 2 (𝜏𝜒)
53, 4syl6ibr 240 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  3anim123d  1397  3orim123d  1398  mo3  2494  moim  2506  2euswap  2535  nelcon3d  2894  ral2imi  2930  ralimdv2  2943  rexim  2990  reximd2a  2995  reximdv2  2996  moeq3  3349  rmoim  3373  2reuswap  3376  ssel  3561  sstr2  3574  ssrexf  3627  sscon  3705  ssdif  3706  unss1  3743  ssrin  3799  difin0ss  3899  r19.2z  4011  prel12  4318  uniss  4388  ssuni  4389  ssuniOLD  4390  intssuni  4428  iunss1  4462  iinss1  4463  ss2iun  4466  iunxdif3  4536  disjss2  4550  disjss1  4553  disjss3  4576  ssbrd  4620  sspwb  4838  poss  4951  pofun  4965  soss  4967  frss  4995  sess1  4996  sess2  4997  wess  5015  relss  5119  ssrel  5120  ssrel2  5122  ssrelrel  5132  relop  5182  cnvssOLD  5205  dmss  5232  dmcosseq  5295  funss  5808  fss  5955  fun  5965  brprcneu  6081  f1eqcocnv  6434  isores3  6463  isomin  6465  isopolem  6473  isosolem  6475  isowe2  6478  ovmpt2s  6660  dfwe2  6850  onint  6864  orduniorsuc  6899  ordom  6943  finds  6961  finds2  6963  f1oweALT  7020  tposfn2  7238  tposfo2  7239  tposf1o2  7242  smores  7313  tz7.48lem  7400  tz7.48-3  7403  oaass  7505  iiner  7683  xpdom2  7917  ssenen  7996  pssnn  8040  hartogs  8309  card2on  8319  ackbij1  8920  cfub  8931  fin23lem27  9010  fin1a2lem11  9092  fin1a2lem13  9094  hsmexlem2  9109  zorn2lem4  9181  ondomon  9241  gchina  9377  intgru  9492  ingru  9493  addclprlem2  9695  psslinpr  9709  ltexprlem3  9716  ltexprlem4  9717  reclem2pr  9726  suplem1pr  9730  sup2  10828  nnind  10885  nnunb  11135  uzind  11301  xmullem2  11924  xrsupsslem  11965  xrinfmsslem  11966  seqof  12675  hashfacen  13047  sswrd  13114  wrdind  13274  wrd2ind  13275  swrdccatin12lem2  13286  cau3lem  13888  caubnd  13892  sumodd  14895  vdwnnlem2  15484  ramub2  15502  setsstruct  15673  fthres2  16361  odupos  16904  lsmdisj2  17864  pgpfac1lem3  18245  subrgdvds  18563  lspdisj  18892  lspprat  18920  lbsextlem2  18926  coe1fzgsumd  19439  evl1gsumd  19488  ocv2ss  19778  ocvin  19779  tgcl  20526  epttop  20565  cmpsub  20955  tgcmp  20956  hauscmplem  20961  dfcon2  20974  llyss  21034  nllyss  21035  locfincmp  21081  txcnpi  21163  txcnp  21175  snfil  21420  fgcl  21434  filcon  21439  filuni  21441  cfinfil  21449  csdfil  21450  supfil  21451  ufildom1  21482  fin1aufil  21488  fmfnfmlem3  21512  ptcmplem2  21609  cldsubg  21666  iscau3  22802  iscau4  22803  caussi  22821  volfiniun  23039  plycj  23754  abelth  23916  wilthlem2  24512  lgsdir2lem4  24770  gausslemma2dlem0i  24806  gausslemma2dlem1a  24807  pntleml  25017  cusgrafilem2  25774  frisusgranb  26290  frgrancvvdeqlem3  26325  lpni  26488  ubthlem1  26916  chintcli  27380  h1de2i  27602  spansnm0i  27699  strlem1  28299  mdslmd1i  28378  2reuswap2  28518  ssrmo  28524  rabss3d  28542  disjss1f  28574  disjpreima  28585  ssrelf  28611  suppss3  28696  nnindf  28758  oduprs  28793  crefss  29050  esumpcvgval  29273  derangenlem  30213  conpcon  30277  cvmsss2  30316  pocnv  30713  wzel  30821  wzelOLD  30822  sltres  30867  nocvxmin  30896  naim1  31360  naim2  31361  waj-ax  31389  lukshef-ax2  31390  bj-ssbim  31616  bj-mo3OLD  31828  poimirlem26  32401  poimirlem30  32405  poimirlem32  32407  itg2addnclem  32427  ismtybndlem  32571  ablo4pnp  32645  isdrngo3  32724  keridl  32797  ispridl2  32803  ispridlc  32835  prter1  32978  lshpdisj  33088  snatpsubN  33850  pmapglb2N  33871  pmapglb2xN  33872  elpaddn0  33900  mzpindd  36123  pellexlem3  36209  pellexlem5  36211  pellex  36213  2nn0ind  36324  lnr2i  36501  intabssd  36731  iunrelexpuztr  36826  hess  36890  frege52aid  36968  frege52b  36999  neik0pk1imk0  37161  2rmoswap  39630  pfxccatin12lem2  40085  uhgr0vsize0  40460  cusgrfilem2  40667  uhgrvd00  40745  clwwisshclwws  41230  frcond3  41435  frgrncvvdeqlem3  41466  nrhmzr  41658
  Copyright terms: Public domain W3C validator