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  1358  mp3an12  1361  mp3an13  1362  ax9o  1744  sbnfc2  3185  ssdifss  3334  undifss  3572  uneqdifeqim  3577  elssuni  3916  csbexa  4213  difexg  4225  rabexg  4227  abssexg  4266  snexg  4268  copsexg  4330  sotritric  4415  sotritrieq  4416  trsuc  4513  oneli  4519  unexb  4533  opeluu  4541  rabxfr  4561  reuhyp  4563  ordunisuc2r  4606  reg3exmid  4672  brrelex12i  4761  brrelex1i  4762  brrelex2i  4763  xpss2  4830  opabid2  4853  eliunxp  4861  releldmi  4963  relelrni  4964  dmexg  4988  rnexg  4989  elres  5041  resexg  5045  relbrcnvg  5107  brcodir  5116  sotri  5124  sotri2  5126  sotri3  5127  dfrel2  5179  coi1  5244  fco  5491  fssres  5503  fabexg  5515  fvopab3g  5709  mptrcl  5719  mpteqb  5727  elfvmptrab1  5731  ffvelcdmi  5771  fsn2  5811  dfmptg  5816  fcof  5822  fvpr1  5847  fvconst2  5859  mptexg  5868  oprabid  6039  ovprc  6043  caovcl  6166  caovass  6172  caovdi  6191  elmpocl  6206  relmptopab  6213  ofexg  6229  resfunexgALT  6259  fo1stresm  6313  fo2ndresm  6314  1stexg  6319  2ndexg  6320  elopabi  6347  mpoexxg  6362  mpoxopn0yelv  6391  rntpos  6409  smores  6444  tfr0dm  6474  tfrlemibxssdm  6479  tfrexlem  6486  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  rdgruledefgg  6527  rdgruledefg  6528  rdgivallem  6533  rdgexg  6541  frec0g  6549  ordgt0ge1  6589  omfnex  6603  oeiv  6610  nna0r  6632  nnm0r  6633  nnsucsssuc  6646  nn2m  6681  nnaordex  6682  nnawordex  6683  ecdmn0m  6732  ecelqsi  6744  ecidg  6754  ectocl  6757  encv  6901  f1oen  6918  ssdomg  6938  map1  6973  fiprc  6976  dom1o  6985  xpdom1  7002  fict  7038  isinfinf  7067  ac6sfi  7068  xpfi  7102  en1eqsn  7123  fidcenumlemr  7130  fiss  7152  eqinfti  7195  djueq2  7216  djulclr  7224  djurclr  7225  djulcl  7226  djurcl  7227  djuf1olem  7228  djulclb  7230  inl11  7240  eldju1st  7246  1stinl  7249  2ndinl  7250  1stinr  7251  2ndinr  7252  ctssdccl  7286  isomnimap  7312  ismkvmap  7329  iswomnimap  7341  finacn  7394  djucomen  7406  exmidapne  7454  0nnq  7559  mulidnq  7584  archnqq  7612  prarloclemarch2  7614  nqnq0pi  7633  nq0m0r  7651  nq02m  7660  prarloclemlt  7688  prarloclemn  7694  prarloclem5  7695  addnqprllem  7722  addnqprulem  7723  appdivnq  7758  1idprl  7785  1idpru  7786  addextpr  7816  cauappcvgprlemdisj  7846  cauappcvgprlemloc  7847  cauappcvgprlemladdru  7851  cauappcvgprlemladdrl  7852  caucvgprlemnbj  7862  caucvgprlemloc  7870  caucvgprprlemnbj  7888  caucvgprprlemloc  7898  caucvgprprlemaddq  7903  suplocexprlemmu  7913  suplocexprlemru  7914  suplocexprlemloc  7916  suplocexprlemlub  7919  0nsr  7944  ltsosr  7959  recexgt0sr  7968  prsrpos  7980  caucvgsr  7997  mappsrprg  7999  suplocsrlem  8003  mulresr  8033  axcnre  8076  axpre-ltwlin  8078  mullid  8152  0re  8154  axmulgt0  8226  ltnsym2  8245  eqlei  8248  ltnei  8258  muladd11  8287  cnegex  8332  0cnALT  8344  negcl  8354  negneg  8404  mul02  8541  mulm1  8554  lt0neg2  8624  le0neg2  8626  recexre  8733  recexgt0  8735  mulge0  8774  gt0ap0i  8782  recextlem1  8806  recexap  8808  recclapzi  8892  recap0apzi  8893  recidapzi  8894  divassapzi  8917  divmulapzi  8918  divdirapzi  8919  rerecclapzi  8931  ltp1  8999  recgt0i  9061  ltmul1i  9075  ltdiv1i  9076  ltmuldivi  9077  ltmul2i  9078  lemul1i  9079  lemul2i  9080  sup3exmid  9112  nngt1ne1  9153  nnrecre  9155  nn0ge0  9402  nn0addcl  9412  nn0mulcl  9413  zgt0ge1  9513  dfuzi  9565  eluzel2  9735  eluz2b1  9804  uz2m1nn  9808  elnn0dc  9814  elnndc  9815  nn01to3  9820  zq  9829  nnrecq  9848  rpge0  9870  rpreccl  9884  mnflt  9987  pnfnlt  9991  mnfle  9996  xrlelttr  10010  xrltletr  10011  xrletr  10012  xgepnf  10020  xlt0neg2  10043  xle0neg2  10045  xaddpnf2  10051  xaddmnf2  10053  xaddid2  10067  elioomnf  10172  ige3m2fz  10253  fzshftral  10312  ige2m1fz1  10313  1fv  10343  4fvwrd4  10344  rebtwn2zlemstep  10480  qbtwnxr  10485  btwnzge0  10528  zmodid2  10582  q2txmodxeq0  10614  frec2uzrand  10635  frecuzrdgtcl  10642  frecfzennn  10656  nn0ennn  10663  uzennn  10666  0exp  10804  sqgt0api  10855  subsq2  10877  qsqeqor  10880  bernneq  10890  faclbnd  10971  faclbnd2  10972  faclbnd3  10973  hashinfuni  11007  hashxp  11056  iswrdiz  11086  lsw0  11127  ccatlid  11149  s1leng  11165  s1fv  11167  s111  11172  pfx0g  11216  2shfti  11350  reim  11371  imcl  11373  crim  11377  caucvgre  11500  rennim  11521  resqrexlemdecn  11531  qabsor  11594  absimle  11603  sqrtthi  11638  sqrtcli  11639  sqrtgt0i  11640  sqrtmsqi  11641  sqrtsqi  11642  sqsqrti  11643  sqrtge0i  11644  absidi  11645  absnidi  11646  xrmaxiflemlub  11767  serclim0  11824  fsum2d  11954  fsumcnv  11956  fsumconst  11973  modfsummodlem1  11975  fsumabs  11984  binom11  12005  prodf1  12061  prodfclim1  12063  prodsnf  12111  fprod2d  12142  fprodcnv  12144  efzval  12202  eftlub  12209  efsep  12210  ef4p  12213  efgt1  12216  reef11  12218  sinf  12223  cosf  12224  efi4p  12236  sinneg  12245  cosneg  12246  efival  12251  efmival  12252  cos01gt0  12282  sin02gt0  12283  absefib  12290  efieq1re  12291  demoivre  12292  demoivreALT  12293  eirraplem  12296  0dvds  12330  odd2np1lem  12391  odd2np1  12392  even2n  12393  mod2eq0even  12397  2teven  12406  opoe  12414  omoe  12415  opeo  12416  omeo  12417  m1exp1  12420  bits0e  12468  bits0o  12469  bitsinv1  12481  gcd0id  12508  gcdid0  12509  1gcd  12521  lcmdvds  12609  isprm2lem  12646  isprm3  12648  prmgt1  12662  coprm  12674  isevengcd2  12688  isoddgcd1  12689  sqpweven  12705  2sqpwodd  12706  pythagtriplem12  12806  pythagtriplem13  12807  pythagtriplem14  12808  pythagtriplem16  12810  pc2dvds  12861  oddprmdvds  12885  pockthi  12889  1arith2  12899  unennn  12976  ctinfomlemom  13006  qnnen  13010  ssnnctlemct  13025  strslfv  13085  strle1g  13147  1strbas  13158  tgval  13303  ismgmn0  13399  mulgval  13667  mulgfng  13669  mulg0  13670  mulg1  13674  mulg2  13676  isnsg  13747  ringidvalg  13932  issrg  13936  subrgpropd  14225  rrgval  14234  islmod  14263  scaffvalg  14278  islssm  14329  sraval  14409  mopnset  14524  metuex  14527  zrhval  14589  zrhvalg  14590  zrhex  14593  psrbag  14641  istopon  14695  eltg4i  14737  eltg3  14739  tg1  14741  tg2  14742  topnex  14768  cldrcl  14784  restsn  14862  lmrcl  14874  metflem  15031  xmetf  15032  ismet2  15036  xmeteq0  15041  xmettri2  15043  xmetpsmet  15051  xmetres2  15061  blfvalps  15067  blex  15069  blvalps  15070  blval  15071  blfps  15091  blf  15092  mopnval  15124  cnbl0  15216  cnblcld  15217  blssioo  15235  resubmet  15238  cncfmet  15274  cnplimcim  15349  cnlimcim  15353  cnlimc  15354  dvfgg  15370  dvfpm  15371  dvfcnpm  15372  dvcj  15391  dvmptfsum  15407  reeff1olem  15453  ef2kpi  15488  sinperlem  15490  sin2kpi  15493  cos2kpi  15494  sinhalfpip  15502  sinhalfpim  15503  coshalfpip  15504  coshalfpim  15505  sincosq1sgn  15508  sinq12gt0  15512  sinkpi  15529  reeflog  15545  relogef  15546  logrpap0b  15558  loggt0b  15573  1cxp  15582  ecxp  15583  2logb9irrap  15659  0sgm  15667  lgsval2lem  15697  m1lgs  15772  1vgrex  15829  upgrfi  15910  umgredgnlp  15958  wlkop  16069  djucllem  16188  bdrabexg  16293  bdunexb  16307  peano5set  16327  speano5  16331  bj-omtrans  16343  pw1ninf  16384  pwf1oexmid  16394  nninfsellemeq  16410  iswomninnlem  16447