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  6525  addnqpr1lemil  6539  addnqpr1lemiu  6540  addnqpr1  6541  1idprl  6564  1idpru  6565  1idpr  6566  recexprlem1ssl  6603  recexprlem1ssu  6604  ltmprr  6612  0idsr  6655  1idsr  6656  00sr  6657  pn0sr  6659  negexsr  6660  recexgt0sr  6661  archsr  6668  pitonnlem1p1  6702  ax1rid  6721  axcnre  6725  peano2cn  6905  peano2re  6906  addid2  6909  subid  6986  subid1  6987  negid  7014  negeq0  7021  peano2cnm  7033  peano2rem  7034  mul01  7142  lt0neg1  7218  le0neg1  7220  recexre  7322  inelr  7328  rimul  7329  reapmul1  7339  apsqgt0  7345  mulge0  7363  negap0  7372  divvalap  7395  rerecclap  7448  div2negap  7453  divgt0i2i  7624  peano5nni  7658  nnge1  7678  times2  7777  addltmul  7898  nn0p1nn  7957  peano2nn0  7958  nn0lele2xi  7969  znnnlt1  8029  nn0lt10b  8057  prime  8073  msqznn  8074  zeo  8079  elnn1uz2  8280  qreccl  8311  qdivcl  8312  irrmul  8316  rphalfcl  8345  rpnegap  8350  ltpnf  8432  nltmnf  8439  pnfge  8440  xlt0neg1  8481  xle0neg1  8483  elioopnf  8566  elicopnf  8568  iccshftri  8593  iccshftli  8595  iccdili  8597  icccntri  8599  fzprval  8674  fzofzp1  8813  fzostep1  8823  frecuzrdgsuc  8842  expivallem  8870  expival  8871  exp1  8875  qexpclz  8890  nn0sqcl  8896  expeq0  8900  expubnd  8925  sqval  8926  sqeq0  8931  resqcl  8934  zsqcl  8937  binom21  8976  reim0  9049  imval2  9082  cjap0  9095  cjne0  9096  bj-inf2vnlem1  9354