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  1219  mp3an12  1222  mp3an13  1223  ax9o  1588  sbnfc2  2906  ssdifss  3074  undifss  3303  uneqdifeqim  3308  elssuni  3608  csbexa  3886  difexg  3898  rabexg  3900  abssexg  3934  snexgOLD  3935  snexg  3936  copsexg  3981  sotritric  4061  sotritrieq  4062  trsuc  4159  oneli  4165  unexb  4177  opeluu  4182  rabxfr  4202  reuhyp  4204  ordunisuc2r  4240  reg3exmid  4304  brrelexi  4384  brrelex2i  4385  xpss2  4449  opabid2  4467  eliunxp  4475  releldmi  4573  relelrni  4574  dmexg  4596  rnexg  4597  elres  4646  resexg  4650  relbrcnvg  4704  brcodir  4712  sotri  4720  sotri2  4722  sotri3  4723  dfrel2  4771  coi1  4836  fco  5056  fssres  5066  fabexg  5077  fvopab3g  5245  mpteqb  5261  ffvelrni  5301  fsn2  5337  dfmptg  5342  fvpr1  5365  fvconst2  5377  mptexg  5386  oprabid  5537  ovprc  5540  caovcl  5655  caovass  5661  caovdi  5680  elmpt2cl  5698  ofexg  5716  resfunexgALT  5737  fo1stresm  5788  fo2ndresm  5789  1stexg  5794  2ndexg  5795  elopabi  5821  mpt2exxg  5833  mpt2xopn0yelv  5854  rntpos  5872  smores  5907  tfr0  5937  tfrlemibxssdm  5941  tfrexlem  5948  rdgruledefgg  5962  rdgruledefg  5963  rdgivallem  5968  rdgon  5973  rdgexg  5976  frec0g  5983  ordgt0ge1  6018  omfnex  6029  oeiv  6036  oeicl  6042  nna0r  6057  nnm0r  6058  nnsucsssuc  6071  nn2m  6099  nnaordex  6100  nnawordex  6101  ecdmn0m  6148  ecelqsi  6160  ecidg  6170  ectocl  6173  encv  6227  f1oen  6239  ssdomg  6258  fiprc  6292  xpdom1  6309  ac6sfi  6352  0nnq  6462  mulidnq  6487  archnqq  6515  prarloclemarch2  6517  nqnq0pi  6536  nq0m0r  6554  nq02m  6563  prarloclemlt  6591  prarloclemn  6597  prarloclem5  6598  addnqprllem  6625  addnqprulem  6626  appdivnq  6661  1idprl  6688  1idpru  6689  addextpr  6719  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemnbj  6765  caucvgprlemloc  6773  caucvgprprlemnbj  6791  caucvgprprlemloc  6801  caucvgprprlemaddq  6806  0nsr  6834  ltsosr  6849  recexgt0sr  6858  prsrpos  6869  caucvgsr  6886  mulresr  6914  axcnre  6955  axpre-ltwlin  6957  mulid2  7025  0re  7027  axmulgt0  7091  ltnsym2  7108  eqlei  7111  ltnei  7121  muladd11  7146  cnegex  7189  0cnALT  7201  negcl  7211  negneg  7261  mul02  7384  mulm1  7397  lt0neg2  7464  le0neg2  7466  recexre  7569  recexgt0  7571  mulge0  7610  gt0ap0i  7617  recextlem1  7632  recexap  7634  recclapzi  7713  recap0apzi  7714  recidapzi  7715  divassapzi  7738  divmulapzi  7739  divdirapzi  7740  rerecclapzi  7752  ltp1  7810  recgt0i  7872  ltmul1i  7886  ltdiv1i  7887  ltmuldivi  7888  ltmul2i  7889  lemul1i  7890  lemul2i  7891  nngt1ne1  7948  nnrecre  7950  nn0ge0  8207  nn0addcl  8217  nn0mulcl  8218  zgt0ge1  8302  dfuzi  8348  eluzel2  8478  eluz2b1  8539  uz2m1nn  8542  nn01to3  8552  zq  8561  nnrecq  8579  rpge0  8595  rpreccl  8609  mnflt  8704  pnfnlt  8708  mnfle  8713  xrlelttr  8722  xrltletr  8723  xrletr  8724  xlt0neg2  8752  xle0neg2  8754  elioomnf  8837  ige3m2fz  8913  fzshftral  8970  ige2m1fz1  8971  1fv  8996  4fvwrd4  8997  rebtwn2zlemstep  9107  btwnzge0  9142  frec2uzrand  9191  frecuzrdgfn  9198  frecuzrdgsuc  9201  frecfzennn  9203  nn0ennn  9209  iseqeq4  9217  expival  9257  0exp  9290  sqgt0api  9339  subsq2  9359  bernneq  9369  2shfti  9432  reim  9452  imcl  9454  crim  9458  caucvgre  9580  rennim  9600  resqrexlemdecn  9610  absimle  9680  sqrtthi  9715  sqrtcli  9716  sqrtgt0i  9717  sqrtmsqi  9718  sqrtsqi  9719  sqsqrti  9720  sqrtge0i  9721  absidi  9722  absnidi  9723  iserclim0  9826  bdrabexg  10026  bdunexb  10040  peano5set  10064  speano5  10069  bj-omtrans  10081