Theorem mpan 424

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  mp2an  426  mpanl12  436  mp3an1  1324  mp3an12  1327  mp3an13  1328  ax9o  1698  sbnfc2  3118  ssdifss  3266  undifss  3504  uneqdifeqim  3509  elssuni  3838  csbexa  4133  difexg  4145  rabexg  4147  abssexg  4183  snexg  4185  copsexg  4245  sotritric  4325  sotritrieq  4326  trsuc  4423  oneli  4429  unexb  4443  opeluu  4451  rabxfr  4471  reuhyp  4473  ordunisuc2r  4514  reg3exmid  4580  brrelex12i  4669  brrelex1i  4670  brrelex2i  4671  xpss2  4738  opabid2  4759  eliunxp  4767  releldmi  4867  relelrni  4868  dmexg  4892  rnexg  4893  elres  4944  resexg  4948  relbrcnvg  5008  brcodir  5017  sotri  5025  sotri2  5027  sotri3  5028  dfrel2  5080  coi1  5145  fco  5382  fssres  5392  fabexg  5404  fvopab3g  5590  mptrcl  5599  mpteqb  5607  elfvmptrab1  5611  ffvelcdmi  5651  fsn2  5691  dfmptg  5696  fvpr1  5721  fvconst2  5733  mptexg  5742  oprabid  5907  ovprc  5910  caovcl  6029  caovass  6035  caovdi  6054  elmpocl  6069  ofexg  6087  resfunexgALT  6109  fo1stresm  6162  fo2ndresm  6163  1stexg  6168  2ndexg  6169  elopabi  6196  mpoexxg  6211  mpoxopn0yelv  6240  rntpos  6258  smores  6293  tfr0dm  6323  tfrlemibxssdm  6328  tfrexlem  6335  tfr1onlembxssdm  6344  tfrcllembxssdm  6357  rdgruledefgg  6376  rdgruledefg  6377  rdgivallem  6382  rdgexg  6390  frec0g  6398  ordgt0ge1  6436  omfnex  6450  oeiv  6457  nna0r  6479  nnm0r  6480  nnsucsssuc  6493  nn2m  6528  nnaordex  6529  nnawordex  6530  ecdmn0m  6577  ecelqsi  6589  ecidg  6599  ectocl  6602  encv  6746  f1oen  6759  ssdomg  6778  map1  6812  fiprc  6815  xpdom1  6835  fict  6868  isinfinf  6897  ac6sfi  6898  xpfi  6929  en1eqsn  6947  fidcenumlemr  6954  fiss  6976  eqinfti  7019  djueq2  7040  djulclr  7048  djurclr  7049  djulcl  7050  djurcl  7051  djuf1olem  7052  djulclb  7054  inl11  7064  eldju1st  7070  1stinl  7073  2ndinl  7074  1stinr  7075  2ndinr  7076  ctssdccl  7110  isomnimap  7135  ismkvmap  7152  iswomnimap  7164  djucomen  7215  exmidapne  7259  0nnq  7363  mulidnq  7388  archnqq  7416  prarloclemarch2  7418  nqnq0pi  7437  nq0m0r  7455  nq02m  7464  prarloclemlt  7492  prarloclemn  7498  prarloclem5  7499  addnqprllem  7526  addnqprulem  7527  appdivnq  7562  1idprl  7589  1idpru  7590  addextpr  7620  cauappcvgprlemdisj  7650  cauappcvgprlemloc  7651  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  caucvgprlemnbj  7666  caucvgprlemloc  7674  caucvgprprlemnbj  7692  caucvgprprlemloc  7702  caucvgprprlemaddq  7707  suplocexprlemmu  7717  suplocexprlemru  7718  suplocexprlemloc  7720  suplocexprlemlub  7723  0nsr  7748  ltsosr  7763  recexgt0sr  7772  prsrpos  7784  caucvgsr  7801  mappsrprg  7803  suplocsrlem  7807  mulresr  7837  axcnre  7880  axpre-ltwlin  7882  mullid  7955  0re  7957  axmulgt0  8029  ltnsym2  8048  eqlei  8051  ltnei  8061  muladd11  8090  cnegex  8135  0cnALT  8147  negcl  8157  negneg  8207  mul02  8344  mulm1  8357  lt0neg2  8426  le0neg2  8428  recexre  8535  recexgt0  8537  mulge0  8576  gt0ap0i  8584  recextlem1  8608  recexap  8610  recclapzi  8694  recap0apzi  8695  recidapzi  8696  divassapzi  8719  divmulapzi  8720  divdirapzi  8721  rerecclapzi  8733  ltp1  8801  recgt0i  8863  ltmul1i  8877  ltdiv1i  8878  ltmuldivi  8879  ltmul2i  8880  lemul1i  8881  lemul2i  8882  sup3exmid  8914  nngt1ne1  8954  nnrecre  8956  nn0ge0  9201  nn0addcl  9211  nn0mulcl  9212  zgt0ge1  9311  dfuzi  9363  eluzel2  9533  eluz2b1  9601  uz2m1nn  9605  elnn0dc  9611  elnndc  9612  nn01to3  9617  zq  9626  nnrecq  9645  rpge0  9666  rpreccl  9680  mnflt  9783  pnfnlt  9787  mnfle  9792  xrlelttr  9806  xrltletr  9807  xrletr  9808  xgepnf  9816  xlt0neg2  9839  xle0neg2  9841  xaddpnf2  9847  xaddmnf2  9849  xaddid2  9863  elioomnf  9968  ige3m2fz  10049  fzshftral  10108  ige2m1fz1  10109  1fv  10139  4fvwrd4  10140  rebtwn2zlemstep  10253  qbtwnxr  10258  btwnzge0  10300  zmodid2  10352  q2txmodxeq0  10384  frec2uzrand  10405  frecuzrdgtcl  10412  frecfzennn  10426  nn0ennn  10433  uzennn  10436  0exp  10555  sqgt0api  10606  subsq2  10628  qsqeqor  10631  bernneq  10641  faclbnd  10721  faclbnd2  10722  faclbnd3  10723  hashinfuni  10757  hashxp  10806  2shfti  10840  reim  10861  imcl  10863  crim  10867  caucvgre  10990  rennim  11011  resqrexlemdecn  11021  qabsor  11084  absimle  11093  sqrtthi  11128  sqrtcli  11129  sqrtgt0i  11130  sqrtmsqi  11131  sqrtsqi  11132  sqsqrti  11133  sqrtge0i  11134  absidi  11135  absnidi  11136  xrmaxiflemlub  11256  serclim0  11313  fsum2d  11443  fsumcnv  11445  fsumconst  11462  modfsummodlem1  11464  fsumabs  11473  binom11  11494  prodf1  11550  prodfclim1  11552  prodsnf  11600  fprod2d  11631  fprodcnv  11633  efzval  11691  eftlub  11698  efsep  11699  ef4p  11702  efgt1  11705  reef11  11707  sinf  11712  cosf  11713  efi4p  11725  sinneg  11734  cosneg  11735  efival  11740  efmival  11741  cos01gt0  11770  sin02gt0  11771  absefib  11778  efieq1re  11779  demoivre  11780  demoivreALT  11781  eirraplem  11784  0dvds  11818  odd2np1lem  11877  odd2np1  11878  even2n  11879  mod2eq0even  11883  2teven  11892  opoe  11900  omoe  11901  opeo  11902  omeo  11903  m1exp1  11906  gcd0id  11980  gcdid0  11981  1gcd  11993  lcmdvds  12079  isprm2lem  12116  isprm3  12118  prmgt1  12132  coprm  12144  isevengcd2  12158  isoddgcd1  12159  sqpweven  12175  2sqpwodd  12176  pythagtriplem12  12275  pythagtriplem13  12276  pythagtriplem14  12277  pythagtriplem16  12279  pc2dvds  12329  oddprmdvds  12352  pockthi  12356  1arith2  12366  unennn  12398  ctinfomlemom  12428  qnnen  12432  ssnnctlemct  12447  strslfv  12507  strle1g  12565  1strbas  12576  tgval  12711  ismgmn0  12777  mulgval  12986  mulgfng  12987  mulg0  12988  mulg1  12990  mulg2  12992  isnsg  13062  ringidvalg  13144  issrg  13148  subrgpropd  13369  islmod  13381  scaffvalg  13396  istopon  13516  eltg4i  13558  eltg3  13560  tg1  13562  tg2  13563  topnex  13589  cldrcl  13605  restsn  13683  lmrcl  13694  metflem  13852  xmetf  13853  ismet2  13857  xmeteq0  13862  xmettri2  13864  xmetpsmet  13872  xmetres2  13882  blfvalps  13888  blex  13890  blvalps  13891  blval  13892  blfps  13912  blf  13913  mopnval  13945  cnbl0  14037  cnblcld  14038  blssioo  14048  resubmet  14051  cncfmet  14082  cnplimcim  14139  cnlimcim  14143  cnlimc  14144  dvfgg  14160  dvfpm  14161  dvfcnpm  14162  dvcj  14176  reeff1olem  14195  ef2kpi  14230  sinperlem  14232  sin2kpi  14235  cos2kpi  14236  sinhalfpip  14244  sinhalfpim  14245  coshalfpip  14246  coshalfpim  14247  sincosq1sgn  14250  sinq12gt0  14254  sinkpi  14271  reeflog  14287  relogef  14288  logrpap0b  14300  loggt0b  14315  1cxp  14324  ecxp  14325  2logb9irrap  14398  lgsval2lem  14414  m1lgs  14455  djucllem  14555  bdrabexg  14661  bdunexb  14675  peano5set  14695  speano5  14699  bj-omtrans  14711  pwf1oexmid  14752  nninfsellemeq  14766  iswomninnlem  14800