Theorem mpan 418

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 416	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  mp2an  420  mpanl12  430  mp3an1  1270  mp3an12  1273  mp3an13  1274  ax9o  1644  sbnfc2  3010  ssdifss  3153  undifss  3390  uneqdifeqim  3395  elssuni  3711  csbexa  3997  difexg  4009  rabexg  4011  abssexg  4046  snexg  4048  copsexg  4104  sotritric  4184  sotritrieq  4185  trsuc  4282  oneli  4288  unexb  4301  opeluu  4309  rabxfr  4329  reuhyp  4331  ordunisuc2r  4368  reg3exmid  4432  brrelex12i  4519  brrelex1i  4520  brrelex2i  4521  xpss2  4588  opabid2  4608  eliunxp  4616  releldmi  4716  relelrni  4717  dmexg  4739  rnexg  4740  elres  4791  resexg  4795  relbrcnvg  4854  brcodir  4862  sotri  4870  sotri2  4872  sotri3  4873  dfrel2  4925  coi1  4990  fco  5224  fssres  5234  fabexg  5246  fvopab3g  5426  mptrcl  5435  mpteqb  5443  elfvmptrab1  5447  ffvelrni  5486  fsn2  5526  dfmptg  5531  fvpr1  5556  fvconst2  5568  mptexg  5577  oprabid  5735  ovprc  5738  caovcl  5857  caovass  5863  caovdi  5882  elmpocl  5900  ofexg  5918  resfunexgALT  5939  fo1stresm  5990  fo2ndresm  5991  1stexg  5996  2ndexg  5997  elopabi  6023  mpoexxg  6038  mpoxopn0yelv  6066  rntpos  6084  smores  6119  tfr0dm  6149  tfrlemibxssdm  6154  tfrexlem  6161  tfr1onlembxssdm  6170  tfrcllembxssdm  6183  rdgruledefgg  6202  rdgruledefg  6203  rdgivallem  6208  rdgexg  6216  frec0g  6224  ordgt0ge1  6262  omfnex  6275  oeiv  6282  nna0r  6304  nnm0r  6305  nnsucsssuc  6318  nn2m  6352  nnaordex  6353  nnawordex  6354  ecdmn0m  6401  ecelqsi  6413  ecidg  6423  ectocl  6426  encv  6570  f1oen  6583  ssdomg  6602  map1  6636  fiprc  6639  xpdom1  6658  fict  6691  isinfinf  6720  ac6sfi  6721  xpfi  6747  en1eqsn  6764  fidcenumlemr  6771  eqinfti  6822  djueq2  6841  djulclr  6849  djurclr  6850  djulcl  6851  djurcl  6852  djuf1olem  6853  djulclb  6855  inl11  6865  eldju1st  6871  1stinl  6874  2ndinl  6875  1stinr  6876  2ndinr  6877  ctssdclemr  6911  isomnimap  6921  ismkvmap  6940  djucomen  6976  0nnq  7073  mulidnq  7098  archnqq  7126  prarloclemarch2  7128  nqnq0pi  7147  nq0m0r  7165  nq02m  7174  prarloclemlt  7202  prarloclemn  7208  prarloclem5  7209  addnqprllem  7236  addnqprulem  7237  appdivnq  7272  1idprl  7299  1idpru  7300  addextpr  7330  cauappcvgprlemdisj  7360  cauappcvgprlemloc  7361  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  caucvgprlemnbj  7376  caucvgprlemloc  7384  caucvgprprlemnbj  7402  caucvgprprlemloc  7412  caucvgprprlemaddq  7417  0nsr  7445  ltsosr  7460  recexgt0sr  7469  prsrpos  7480  caucvgsr  7497  mulresr  7525  axcnre  7566  axpre-ltwlin  7568  mulid2  7636  0re  7638  axmulgt0  7708  ltnsym2  7725  eqlei  7728  ltnei  7738  muladd11  7766  cnegex  7811  0cnALT  7823  negcl  7833  negneg  7883  mul02  8016  mulm1  8029  lt0neg2  8098  le0neg2  8100  recexre  8206  recexgt0  8208  mulge0  8247  gt0ap0i  8255  recextlem1  8273  recexap  8275  recclapzi  8358  recap0apzi  8359  recidapzi  8360  divassapzi  8383  divmulapzi  8384  divdirapzi  8385  rerecclapzi  8397  ltp1  8460  recgt0i  8522  ltmul1i  8536  ltdiv1i  8537  ltmuldivi  8538  ltmul2i  8539  lemul1i  8540  lemul2i  8541  sup3exmid  8573  nngt1ne1  8613  nnrecre  8615  nn0ge0  8854  nn0addcl  8864  nn0mulcl  8865  zgt0ge1  8964  dfuzi  9013  eluzel2  9181  eluz2b1  9245  uz2m1nn  9249  nn01to3  9259  zq  9268  nnrecq  9287  rpge0  9303  rpreccl  9317  mnflt  9410  pnfnlt  9414  mnfle  9419  xrlelttr  9430  xrltletr  9431  xrletr  9432  xgepnf  9440  xlt0neg2  9463  xle0neg2  9465  xaddpnf2  9471  xaddmnf2  9473  xaddid2  9487  elioomnf  9592  ige3m2fz  9670  fzshftral  9729  ige2m1fz1  9730  1fv  9757  4fvwrd4  9758  rebtwn2zlemstep  9871  qbtwnxr  9876  btwnzge0  9914  zmodid2  9966  q2txmodxeq0  9998  frec2uzrand  10019  frecuzrdgtcl  10026  frecfzennn  10040  nn0ennn  10047  uzennn  10050  0exp  10169  sqgt0api  10219  subsq2  10241  bernneq  10253  faclbnd  10328  faclbnd2  10329  faclbnd3  10330  hashinfuni  10364  hashxp  10413  2shfti  10444  reim  10465  imcl  10467  crim  10471  caucvgre  10593  rennim  10614  resqrexlemdecn  10624  qabsor  10687  absimle  10696  sqrtthi  10731  sqrtcli  10732  sqrtgt0i  10733  sqrtmsqi  10734  sqrtsqi  10735  sqsqrti  10736  sqrtge0i  10737  absidi  10738  absnidi  10739  xrmaxiflemlub  10856  serclim0  10913  fsum2d  11043  fsumcnv  11045  fsumconst  11062  modfsummodlem1  11064  fsumabs  11073  binom11  11094  efzval  11187  eftlub  11194  efsep  11195  ef4p  11198  efgt1  11201  reef11  11204  sinf  11209  cosf  11210  efi4p  11222  sinneg  11231  cosneg  11232  efival  11237  efmival  11238  cos01gt0  11267  sin02gt0  11268  absefib  11274  efieq1re  11275  demoivre  11276  demoivreALT  11277  eirraplem  11278  0dvds  11308  odd2np1lem  11364  odd2np1  11365  even2n  11366  mod2eq0even  11370  2teven  11379  opoe  11387  omoe  11388  opeo  11389  omeo  11390  m1exp1  11393  gcd0id  11462  gcdid0  11463  1gcd  11475  lcmdvds  11553  isprm2lem  11590  isprm3  11592  prmgt1  11605  coprm  11615  isevengcd2  11629  isoddgcd1  11630  sqpweven  11645  2sqpwodd  11646  unennn  11702  ctinfomlemom  11732  qnnen  11736  strslfv  11785  strle1g  11831  1strbas  11840  istopon  11962  tgval  12000  eltg4i  12006  eltg3  12008  tg1  12010  tg2  12011  topnex  12037  cldrcl  12053  restsn  12131  lmrcl  12142  metflem  12277  xmetf  12278  ismet2  12282  xmeteq0  12287  xmettri2  12289  xmetpsmet  12297  xmetres2  12307  blfvalps  12313  blex  12315  blvalps  12316  blval  12317  blfps  12337  blf  12338  mopnval  12370  cnbl0  12456  cnblcld  12457  blssioo  12464  resubmet  12467  cncfmet  12492  cnplimcim  12516  cnlimcim  12517  dvfgg  12530  dvfpm  12531  dvfcnpm  12532  djucllem  12588  bdrabexg  12685  bdunexb  12699  peano5set  12723  speano5  12727  bj-omtrans  12739  pwf1oexmid  12780  nninfsellemeq  12794