Theorem mpan 400

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 399	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  402  mpanl12  412  mp3an1  1218  mp3an12  1221  mp3an13  1222  ax9o  1585  sbnfc2  2900  ssdifss  3068  undifss  3297  uneqdifeqim  3302  elssuni  3599  csbexa  3877  difexg  3889  rabexg  3891  abssexg  3925  snexgOLD  3926  snexg  3927  copsexg  3972  sotritric  4052  sotritrieq  4053  trsuc  4125  oneli  4131  unexb  4143  opeluu  4148  rabxfr  4168  reuhyp  4170  ordunisuc2r  4205  brrelexi  4327  brrelex2i  4328  xpss2  4392  opabid2  4410  eliunxp  4418  releldmi  4516  relelrni  4517  dmexg  4539  rnexg  4540  elres  4589  resexg  4593  relbrcnvg  4647  brcodir  4655  sotri  4663  sotri2  4665  sotri3  4666  dfrel2  4714  coi1  4779  fco  4999  fssres  5009  fabexg  5020  fvopab3g  5188  mpteqb  5204  ffvelrni  5244  fsn2  5280  dfmptg  5285  fvpr1  5308  fvconst2  5320  mptexg  5329  oprabid  5480  ovprc  5482  caovcl  5597  caovass  5603  caovdi  5622  elmpt2cl  5640  ofexg  5658  resfunexgALT  5679  fo1stresm  5730  fo2ndresm  5731  1stexg  5736  2ndexg  5737  elopabi  5763  mpt2exxg  5775  mpt2xopn0yelv  5795  rntpos  5813  smores  5848  tfr0  5878  tfrlemibxssdm  5882  tfrexlem  5889  rdgruledefgg  5902  rdgruledefg  5903  rdgivallem  5908  rdgon  5913  rdgexg  5916  frec0g  5922  ordgt0ge1  5957  omfnex  5968  oeiv  5975  oeicl  5981  nna0r  5996  nnm0r  5997  nnsucsssuc  6010  nn2m  6035  nnaordex  6036  nnawordex  6037  ecdmn0m  6084  ecelqsi  6096  ecidg  6106  ectocl  6109  encv  6163  f1oen  6175  ssdomg  6194  fiprc  6228  xpdom1  6245  0nnq  6348  mulidnq  6373  archnqq  6400  prarloclemarch2  6402  nqnq0pi  6420  nq0m0r  6438  nq02m  6447  prarloclemlt  6475  prarloclemn  6481  prarloclem5  6482  addnqprllem  6509  addnqprulem  6510  appdivnq  6543  1idprl  6565  1idpru  6566  addextpr  6592  cauappcvgprlemdisj  6622  cauappcvgprlemloc  6623  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  0nsr  6657  ltsosr  6672  recexgt0sr  6681  mulresr  6715  axcnre  6745  axpre-ltwlin  6747  mulid2  6803  0re  6805  axmulgt0  6868  ltnsym2  6885  eqlei  6888  ltnei  6898  muladd11  6923  cnegex  6966  0cnALT  6978  negcl  6988  negneg  7037  mul02  7160  mulm1  7173  lt0neg2  7239  le0neg2  7241  recexre  7342  recexgt0  7344  mulge0  7383  gt0ap0i  7389  recextlem1  7394  recexap  7396  recclapzi  7475  recap0apzi  7476  recidapzi  7477  divassapzi  7500  divmulapzi  7501  divdirapzi  7502  rerecclapzi  7514  ltp1  7571  recgt0i  7633  ltmul1i  7647  ltdiv1i  7648  ltmuldivi  7649  ltmul2i  7650  lemul1i  7651  lemul2i  7652  nngt1ne1  7709  nnrecre  7711  nn0ge0  7963  nn0addcl  7973  nn0mulcl  7974  zgt0ge1  8058  dfuzi  8104  eluzel2  8234  eluz2b1  8295  uz2m1nn  8298  nn01to3  8308  zq  8317  nnrecq  8334  rpge0  8350  rpreccl  8364  mnflt  8454  pnfnlt  8458  mnfle  8463  xrlelttr  8472  xrltletr  8473  xrletr  8474  xlt0neg2  8502  xle0neg2  8504  elioomnf  8587  ige3m2fz  8663  fzshftral  8720  ige2m1fz1  8721  1fv  8746  4fvwrd4  8747  frec2uzrand  8852  frecuzrdgfn  8859  frecuzrdgsuc  8862  frecfzennn  8864  nn0ennn  8870  iseqeq4  8877  expival  8891  0exp  8924  sqgt0api  8972  subsq2  8992  bernneq  9002  reim  9060  imcl  9062  crim  9066  rennim  9191  bdrabexg  9337  bdunexb  9351  speano5  9378  bj-omtrans  9390