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  6421  nq0m0r  6439  nq02m  6448  prarloclemlt  6476  prarloclemn  6482  prarloclem5  6483  addnqprllem  6510  addnqprulem  6511  appdivnq  6544  1idprl  6566  1idpru  6567  addextpr  6593  cauappcvgprlemdisj  6623  cauappcvgprlemloc  6624  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  caucvgprlemnbj  6638  caucvgprlemloc  6646  0nsr  6677  ltsosr  6692  recexgt0sr  6701  mulresr  6735  axcnre  6765  axpre-ltwlin  6767  mulid2  6823  0re  6825  axmulgt0  6888  ltnsym2  6905  eqlei  6908  ltnei  6918  muladd11  6943  cnegex  6986  0cnALT  6998  negcl  7008  negneg  7057  mul02  7180  mulm1  7193  lt0neg2  7259  le0neg2  7261  recexre  7362  recexgt0  7364  mulge0  7403  gt0ap0i  7409  recextlem1  7414  recexap  7416  recclapzi  7495  recap0apzi  7496  recidapzi  7497  divassapzi  7520  divmulapzi  7521  divdirapzi  7522  rerecclapzi  7534  ltp1  7591  recgt0i  7653  ltmul1i  7667  ltdiv1i  7668  ltmuldivi  7669  ltmul2i  7670  lemul1i  7671  lemul2i  7672  nngt1ne1  7729  nnrecre  7731  nn0ge0  7983  nn0addcl  7993  nn0mulcl  7994  zgt0ge1  8078  dfuzi  8124  eluzel2  8254  eluz2b1  8315  uz2m1nn  8318  nn01to3  8328  zq  8337  nnrecq  8354  rpge0  8370  rpreccl  8384  mnflt  8474  pnfnlt  8478  mnfle  8483  xrlelttr  8492  xrltletr  8493  xrletr  8494  xlt0neg2  8522  xle0neg2  8524  elioomnf  8607  ige3m2fz  8683  fzshftral  8740  ige2m1fz1  8741  1fv  8766  4fvwrd4  8767  frec2uzrand  8872  frecuzrdgfn  8879  frecuzrdgsuc  8882  frecfzennn  8884  nn0ennn  8890  iseqeq4  8897  expival  8911  0exp  8944  sqgt0api  8992  subsq2  9012  bernneq  9022  reim  9080  imcl  9082  crim  9086  rennim  9211  bdrabexg  9361  bdunexb  9375  peano5set  9399  speano5  9404  bj-omtrans  9416