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

Theorem 3imtr4g 287
Description: More general version of 3imtr4i 283. 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 233 . 2 (𝜑 → (𝜃𝜒))
4 3imtr4g.3 . 2 (𝜏𝜒)
53, 4syl6ibr 243 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  3anim123d  1560  3orim123d  1561  mo3  2677  moim  2689  2euswap  2719  nelcon3d  3100  ral2imi  3142  ralimdv2  3156  rexim  3202  reximd2a  3207  reximdv2  3208  moeq3  3588  rmoim  3612  2reuswap  3615  ssel  3799  sstr2  3812  ssrexf  3869  sscon  3950  ssdif  3951  unss1  3988  ssrin  4041  difin0ss  4154  r19.2z  4262  prel12OLD  4577  uniss  4660  ssuni  4661  intssuni  4698  iunss1  4731  iinss1  4732  ss2iun  4735  iunxdif3  4805  disjss2  4822  disjss1  4825  disjss3  4850  ssbrd  4894  sspwb  5114  poss  5241  pofun  5255  soss  5257  frss  5285  sess1  5286  sess2  5287  wess  5305  relss  5415  ssrelOLD  5417  ssrel2  5419  ssrelrel  5429  relop  5481  dmss  5531  dmcosseq  5595  funss  6123  fss  6272  fun  6284  brprcneu  6403  f1eqcocnv  6783  isores3  6812  isomin  6814  isopolem  6822  isosolem  6824  isowe2  6827  ovmpt2s  7017  dfwe2  7214  onint  7228  orduniorsuc  7263  ordom  7307  finds  7325  finds2  7327  f1oweALT  7385  tposfn2  7612  tposfo2  7613  tposf1o2  7616  smores  7688  tz7.48lem  7775  tz7.48-3  7778  oaass  7881  iiner  8057  xpdom2  8297  ssenen  8376  pssnn  8420  hartogs  8691  card2on  8701  ackbij1  9348  cfub  9359  fin23lem27  9438  fin1a2lem11  9520  fin1a2lem13  9522  hsmexlem2  9537  zorn2lem4  9609  ondomon  9673  gchina  9809  intgru  9924  ingru  9925  addclprlem2  10127  psslinpr  10141  ltexprlem3  10148  ltexprlem4  10149  reclem2pr  10158  suplem1pr  10162  sup2  11267  nnind  11326  nnunb  11558  uzind  11738  xmullem2  12316  xrsupsslem  12358  xrinfmsslem  12359  seqof  13084  hashfacen  13458  sswrd  13527  wrdind  13703  wrd2ind  13704  swrdccatin12lem2  13716  cau3lem  14320  caubnd  14324  sumodd  15334  vdwnnlem2  15920  ramub2  15938  setsstructOLD  16113  fthres2  16799  odupos  17343  lsmdisj2  18299  pgpfac1lem3  18681  subrgdvds  19001  lspdisj  19335  lspprat  19365  lbsextlem2  19371  coe1fzgsumd  19883  evl1gsumd  19932  ocv2ss  20231  ocvin  20232  tgcl  20991  epttop  21031  cmpsub  21421  tgcmp  21422  hauscmplem  21427  dfconn2  21440  llyss  21500  nllyss  21501  locfincmp  21547  txcnpi  21629  txcnp  21641  snfil  21885  fgcl  21899  filconn  21904  filuni  21906  cfinfil  21914  csdfil  21915  supfil  21916  ufildom1  21947  fin1aufil  21953  fmfnfmlem3  21977  ptcmplem2  22074  cldsubg  22131  iscau3  23293  iscau4  23294  caussi  23312  volfiniun  23534  plycj  24253  abelth  24415  wilthlem2  25015  lgsdir2lem4  25273  gausslemma2dlem0i  25309  gausslemma2dlem1a  25310  pntleml  25520  uhgr0vsize0  26353  cusgrfilem2  26586  uhgrvd00  26664  clwwisshclwws  27164  frcond3  27450  frgrncvvdeqlem2  27481  lpni  27669  ubthlem1  28060  chintcli  28524  h1de2i  28746  spansnm0i  28843  strlem1  29443  mdslmd1i  29522  2reuswap2  29660  ssrmo  29666  rabss3d  29682  iinssiun  29708  disjss1f  29717  disjpreima  29728  ssrelf  29758  suppss3  29835  nnindf  29898  oduprs  29987  crefss  30247  esumpcvgval  30471  derangenlem  31481  connpconn  31545  cvmsss2  31584  pocnv  31980  wzel  32095  sltres  32141  nosupno  32175  nocvxmin  32220  naim1  32710  naim2  32711  waj-ax  32735  lukshef-ax2  32736  bj-ssbim  32942  bj-mo3OLD  33147  poimirlem26  33750  poimirlem30  33754  poimirlem32  33756  itg2addnclem  33775  ismtybndlem  33918  ablo4pnp  33992  isdrngo3  34071  keridl  34144  ispridl2  34150  ispridlc  34182  trcoss  34547  prter1  34660  lshpdisj  34769  snatpsubN  35532  pmapglb2N  35553  pmapglb2xN  35554  elpaddn0  35582  mzpindd  37812  pellexlem3  37898  pellexlem5  37900  pellex  37902  2nn0ind  38012  lnr2i  38188  intabssd  38417  iunrelexpuztr  38512  hess  38575  frege52aid  38653  frege52b  38684  neik0pk1imk0  38846  2rmoswap  41697  pfxccatin12lem2  42000  nrhmzr  42442  elsetrecslem  43014
  Copyright terms: Public domain W3C validator