Theorem mpan 402

Description: An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

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

Assertion

Ref	Expression
mpan	⊢ (ψ → χ)

Proof of Theorem mpan

Step	Hyp	Ref	Expression
1		mpan.1	. . 3 ⊢ φ
2	1	a1i 9	. 2 ⊢ (ψ → φ)
3		mpan.2	. 2 ⊢ ((φ ∧ ψ) → χ)
4	2, 3	mpancom 401	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:  mp2an  404  mpanl12  414  mp3an1  1202  mp3an12  1205  mp3an13  1206  ax9o  1566  sbnfc2  2879  ssdifss  3047  undifss  3276  uneqdifeqim  3281  elssuni  3578  csbexOLD  3856  difexg  3868  rabexg  3870  abssexg  3904  snexgOLD  3905  snexg  3906  copsexg  3951  sotritric  4031  sotritrieq  4032  trsuc  4105  oneli  4111  unexb  4123  opeluu  4128  rabxfr  4148  reuhyp  4150  ordunisuc2r  4185  brrelexi  4307  brrelex2i  4308  xpss2  4372  opabid2  4390  eliunxp  4398  releldmi  4496  relelrni  4497  dmexg  4519  rnexg  4520  elres  4569  resexg  4573  relbrcnvg  4627  brcodir  4635  sotri  4643  sotri2  4645  sotri3  4646  dfrel2  4694  coi1  4759  fco  4977  fssres  4987  fabexg  4998  fvopab3g  5166  mpteqb  5182  ffvelrni  5222  fsn2  5258  dfmptg  5263  fvpr1  5286  fvconst2  5298  mptexg  5307  oprabid  5457  ovprc  5459  caovcl  5574  caovass  5580  caovdi  5599  elmpt2cl  5617  ofexg  5635  resfunexgALT  5656  fo1stresm  5707  fo2ndresm  5708  1stexg  5713  2ndexg  5714  elopabi  5740  mpt2exxg  5752  mpt2xopn0yelv  5772  rntpos  5790  smores  5825  tfrlemibxssdm  5858  tfrlemi14  5865  tfrexlem  5866  rdgruledefgg  5878  rdgruledefg  5879  rdgivallem  5884  rdgon  5889  rdgexg  5892  frec0g  5898  ordgt0ge1  5929  omfnex  5940  oeiv  5947  oa0  5948  oei0  5950  oeicl  5953  nna0r  5968  nnm0r  5969  nnsucsssuc  5982  nn2m  6006  nnaordex  6007  nnawordex  6008  ecdmn0m  6055  ecelqsi  6067  ecidg  6077  ectocl  6080  0nnq  6217  mulidnq  6242  archnqq  6268  prarloclemarch2  6270  nqnq0pi  6287  nq0m0r  6305  nq02m  6313  prarloclemlt  6341  prarloclemn  6347  prarloclem5  6348  addnqprllem  6376  addnqprulem  6377  appdivnq  6401  1idprl  6423  1idpru  6424  0nsr  6490  ltsosr  6505  mulresr  6543  axcnre  6569  axpre-ltwlin  6571  mulid2  6621  0re  6623  axmulgt0  6685  ltnsym2  6700  eqlei  6703  ltnei  6711  muladd11  6733  cnegex  6776  0cnALT  6788  negcl  6798  negneg  6847  mul02  6970  mulm1  6983  lt0neg2  7049  le0neg2  7051  bdrabexg  7268  bdunexb  7282  speano5  7305  bj-omtrans  7317