Theorem mpan2 401

Description: An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

Hypotheses

Ref	Expression
mpan2.1	⊢ ψ
mpan2.2	⊢ ((φ ∧ ψ) → χ)

Assertion

Ref	Expression
mpan2	⊢ (φ → χ)

Proof of Theorem mpan2

Step	Hyp	Ref	Expression
1		mpan2.1	. . 3 ⊢ ψ
2	1	a1i 9	. 2 ⊢ (φ → ψ)
3		mpan2.2	. 2 ⊢ ((φ ∧ ψ) → χ)
4	2, 3	mpdan 398	1 ⊢ (φ → χ)

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101

This theorem is referenced by:  mpanr12  415  mp3an23  1223  equs4  1610  sb4bor  1713  eueq2dc  2708  sbcgf  2819  csbconstgf  2857  sbcnestg  2893  csbnestg  2894  csbnest1g  2895  ssindif0im  3275  mpteq1  3832  iinexgm  3899  mss  3953  eusv2nf  4154  eldifpw  4174  ordtriexmid  4210  onsucsssucexmid  4212  ordsucunielexmid  4216  nn0suc  4270  xpss1  4391  xpiindim  4416  reldm0  4496  elrnmpt1s  4527  resdm  4592  resid  4605  eliniseg  4638  trinxp  4661  inimasn  4684  ssrnres  4706  cnveq0  4720  coi2  4780  relrelss  4787  funcnvres  4915  funimaex  4927  fnresin1  4956  fnresin2  4957  fresin  5011  dffv3g  5117  ssimaex  5177  dmfco  5184  fvmpt  5192  fsn  5278  fsn2  5280  elabrex  5340  f1elima  5355  2ndconst  5785  tposfun  5816  tpostpos2  5821  tfrexlem  5889  tfri3  5894  rdgruledefgg  5902  rdgss  5910  frecsuclem3  5929  frecrdg  5931  oa0  5976  om0  5977  oei0  5978  oav2  5982  oa1suc  5986  nnmsucr  6006  nnm1  6033  nnm2  6034  ecelqsg  6095  ecidg  6106  xpiderm  6113  qsel  6119  xp1en  6233  xpcomco  6236  mulidpi  6302  nlt1pig  6325  indpi  6326  halfnqq  6393  archnqq  6400  prarloclemarch  6401  prarloclemarch2  6402  nnnq  6405  nq0a0  6439  addpinq1  6446  prarloclemlt  6475  prarloclemlo  6476  prarloclem3  6479  prarloclemcalc  6484  nqprm  6524  addnqpr1  6542  1idprl  6565  1idpru  6566  1idpr  6567  recexprlem1ssl  6604  recexprlem1ssu  6605  ltmprr  6613  0idsr  6675  1idsr  6676  00sr  6677  pn0sr  6679  negexsr  6680  recexgt0sr  6681  archsr  6688  pitonnlem1p1  6722  ax1rid  6741  axcnre  6745  peano2cn  6925  peano2re  6926  addid2  6929  subid  7006  subid1  7007  negid  7034  negeq0  7041  peano2cnm  7053  peano2rem  7054  mul01  7162  lt0neg1  7238  le0neg1  7240  recexre  7342  inelr  7348  rimul  7349  reapmul1  7359  apsqgt0  7365  mulge0  7383  negap0  7392  divvalap  7415  rerecclap  7468  div2negap  7473  divgt0i2i  7644  peano5nni  7678  nnge1  7698  times2  7797  addltmul  7918  nn0p1nn  7977  peano2nn0  7978  nn0lele2xi  7989  znnnlt1  8049  nn0lt10b  8077  prime  8093  msqznn  8094  zeo  8099  elnn1uz2  8300  qreccl  8331  qdivcl  8332  irrmul  8336  rphalfcl  8365  rpnegap  8370  ltpnf  8452  nltmnf  8459  pnfge  8460  xlt0neg1  8501  xle0neg1  8503  elioopnf  8586  elicopnf  8588  iccshftri  8613  iccshftli  8615  iccdili  8617  icccntri  8619  fzprval  8694  fzofzp1  8833  fzostep1  8843  frecuzrdgsuc  8862  expivallem  8890  expival  8891  exp1  8895  qexpclz  8910  nn0sqcl  8916  expeq0  8920  expubnd  8945  sqval  8946  sqeq0  8951  resqcl  8954  zsqcl  8957  binom21  8996  reim0  9069  imval2  9102  cjap0  9115  cjne0  9116  nn0abscl  9209  bj-inf2vnlem1  9400