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  6440  addpinq1  6447  prarloclemlt  6476  prarloclemlo  6477  prarloclem3  6480  prarloclemcalc  6485  nqprm  6525  addnqpr1  6543  1idprl  6566  1idpru  6567  1idpr  6568  recexprlem1ssl  6605  recexprlem1ssu  6606  ltmprr  6614  0idsr  6695  1idsr  6696  00sr  6697  pn0sr  6699  negexsr  6700  recexgt0sr  6701  archsr  6708  pitonnlem1p1  6742  ax1rid  6761  axcnre  6765  peano2cn  6945  peano2re  6946  addid2  6949  subid  7026  subid1  7027  negid  7054  negeq0  7061  peano2cnm  7073  peano2rem  7074  mul01  7182  lt0neg1  7258  le0neg1  7260  recexre  7362  inelr  7368  rimul  7369  reapmul1  7379  apsqgt0  7385  mulge0  7403  negap0  7412  divvalap  7435  rerecclap  7488  div2negap  7493  divgt0i2i  7664  peano5nni  7698  nnge1  7718  times2  7817  addltmul  7938  nn0p1nn  7997  peano2nn0  7998  nn0lele2xi  8009  znnnlt1  8069  nn0lt10b  8097  prime  8113  msqznn  8114  zeo  8119  elnn1uz2  8320  qreccl  8351  qdivcl  8352  irrmul  8356  rphalfcl  8385  rpnegap  8390  ltpnf  8472  nltmnf  8479  pnfge  8480  xlt0neg1  8521  xle0neg1  8523  elioopnf  8606  elicopnf  8608  iccshftri  8633  iccshftli  8635  iccdili  8637  icccntri  8639  fzprval  8714  fzofzp1  8853  fzostep1  8863  frecuzrdgsuc  8882  expivallem  8910  expival  8911  exp1  8915  qexpclz  8930  nn0sqcl  8936  expeq0  8940  expubnd  8965  sqval  8966  sqeq0  8971  resqcl  8974  zsqcl  8977  binom21  9016  reim0  9089  imval2  9122  cjap0  9135  cjne0  9136  nn0abscl  9229  bj-inf2vnlem1  9430