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  1337  mp3an12  1340  mp3an13  1341  ax9o  1722  sbnfc2  3155  ssdifss  3304  undifss  3542  uneqdifeqim  3547  elssuni  3880  csbexa  4177  difexg  4189  rabexg  4191  abssexg  4230  snexg  4232  copsexg  4292  sotritric  4375  sotritrieq  4376  trsuc  4473  oneli  4479  unexb  4493  opeluu  4501  rabxfr  4521  reuhyp  4523  ordunisuc2r  4566  reg3exmid  4632  brrelex12i  4721  brrelex1i  4722  brrelex2i  4723  xpss2  4790  opabid2  4813  eliunxp  4821  releldmi  4922  relelrni  4923  dmexg  4947  rnexg  4948  elres  5000  resexg  5004  relbrcnvg  5066  brcodir  5075  sotri  5083  sotri2  5085  sotri3  5086  dfrel2  5138  coi1  5203  fco  5447  fssres  5458  fabexg  5470  fvopab3g  5659  mptrcl  5669  mpteqb  5677  elfvmptrab1  5681  ffvelcdmi  5721  fsn2  5761  dfmptg  5766  fvpr1  5795  fvconst2  5807  mptexg  5816  oprabid  5983  ovprc  5987  caovcl  6108  caovass  6114  caovdi  6133  elmpocl  6148  ofexg  6170  resfunexgALT  6200  fo1stresm  6254  fo2ndresm  6255  1stexg  6260  2ndexg  6261  elopabi  6288  mpoexxg  6303  mpoxopn0yelv  6332  rntpos  6350  smores  6385  tfr0dm  6415  tfrlemibxssdm  6420  tfrexlem  6427  tfr1onlembxssdm  6436  tfrcllembxssdm  6449  rdgruledefgg  6468  rdgruledefg  6469  rdgivallem  6474  rdgexg  6482  frec0g  6490  ordgt0ge1  6528  omfnex  6542  oeiv  6549  nna0r  6571  nnm0r  6572  nnsucsssuc  6585  nn2m  6620  nnaordex  6621  nnawordex  6622  ecdmn0m  6671  ecelqsi  6683  ecidg  6693  ectocl  6696  encv  6840  f1oen  6857  ssdomg  6877  map1  6911  fiprc  6914  xpdom1  6937  fict  6972  isinfinf  7001  ac6sfi  7002  xpfi  7036  en1eqsn  7057  fidcenumlemr  7064  fiss  7086  eqinfti  7129  djueq2  7150  djulclr  7158  djurclr  7159  djulcl  7160  djurcl  7161  djuf1olem  7162  djulclb  7164  inl11  7174  eldju1st  7180  1stinl  7183  2ndinl  7184  1stinr  7185  2ndinr  7186  ctssdccl  7220  isomnimap  7246  ismkvmap  7263  iswomnimap  7275  finacn  7323  djucomen  7335  exmidapne  7379  0nnq  7484  mulidnq  7509  archnqq  7537  prarloclemarch2  7539  nqnq0pi  7558  nq0m0r  7576  nq02m  7585  prarloclemlt  7613  prarloclemn  7619  prarloclem5  7620  addnqprllem  7647  addnqprulem  7648  appdivnq  7683  1idprl  7710  1idpru  7711  addextpr  7741  cauappcvgprlemdisj  7771  cauappcvgprlemloc  7772  cauappcvgprlemladdru  7776  cauappcvgprlemladdrl  7777  caucvgprlemnbj  7787  caucvgprlemloc  7795  caucvgprprlemnbj  7813  caucvgprprlemloc  7823  caucvgprprlemaddq  7828  suplocexprlemmu  7838  suplocexprlemru  7839  suplocexprlemloc  7841  suplocexprlemlub  7844  0nsr  7869  ltsosr  7884  recexgt0sr  7893  prsrpos  7905  caucvgsr  7922  mappsrprg  7924  suplocsrlem  7928  mulresr  7958  axcnre  8001  axpre-ltwlin  8003  mullid  8077  0re  8079  axmulgt0  8151  ltnsym2  8170  eqlei  8173  ltnei  8183  muladd11  8212  cnegex  8257  0cnALT  8269  negcl  8279  negneg  8329  mul02  8466  mulm1  8479  lt0neg2  8549  le0neg2  8551  recexre  8658  recexgt0  8660  mulge0  8699  gt0ap0i  8707  recextlem1  8731  recexap  8733  recclapzi  8817  recap0apzi  8818  recidapzi  8819  divassapzi  8842  divmulapzi  8843  divdirapzi  8844  rerecclapzi  8856  ltp1  8924  recgt0i  8986  ltmul1i  9000  ltdiv1i  9001  ltmuldivi  9002  ltmul2i  9003  lemul1i  9004  lemul2i  9005  sup3exmid  9037  nngt1ne1  9078  nnrecre  9080  nn0ge0  9327  nn0addcl  9337  nn0mulcl  9338  zgt0ge1  9438  dfuzi  9490  eluzel2  9660  eluz2b1  9729  uz2m1nn  9733  elnn0dc  9739  elnndc  9740  nn01to3  9745  zq  9754  nnrecq  9773  rpge0  9795  rpreccl  9809  mnflt  9912  pnfnlt  9916  mnfle  9921  xrlelttr  9935  xrltletr  9936  xrletr  9937  xgepnf  9945  xlt0neg2  9968  xle0neg2  9970  xaddpnf2  9976  xaddmnf2  9978  xaddid2  9992  elioomnf  10097  ige3m2fz  10178  fzshftral  10237  ige2m1fz1  10238  1fv  10268  4fvwrd4  10269  rebtwn2zlemstep  10402  qbtwnxr  10407  btwnzge0  10450  zmodid2  10504  q2txmodxeq0  10536  frec2uzrand  10557  frecuzrdgtcl  10564  frecfzennn  10578  nn0ennn  10585  uzennn  10588  0exp  10726  sqgt0api  10777  subsq2  10799  qsqeqor  10802  bernneq  10812  faclbnd  10893  faclbnd2  10894  faclbnd3  10895  hashinfuni  10929  hashxp  10978  iswrdiz  11008  lsw0  11048  ccatlid  11070  s1leng  11086  s1fv  11088  s111  11093  pfx0g  11137  2shfti  11186  reim  11207  imcl  11209  crim  11213  caucvgre  11336  rennim  11357  resqrexlemdecn  11367  qabsor  11430  absimle  11439  sqrtthi  11474  sqrtcli  11475  sqrtgt0i  11476  sqrtmsqi  11477  sqrtsqi  11478  sqsqrti  11479  sqrtge0i  11480  absidi  11481  absnidi  11482  xrmaxiflemlub  11603  serclim0  11660  fsum2d  11790  fsumcnv  11792  fsumconst  11809  modfsummodlem1  11811  fsumabs  11820  binom11  11841  prodf1  11897  prodfclim1  11899  prodsnf  11947  fprod2d  11978  fprodcnv  11980  efzval  12038  eftlub  12045  efsep  12046  ef4p  12049  efgt1  12052  reef11  12054  sinf  12059  cosf  12060  efi4p  12072  sinneg  12081  cosneg  12082  efival  12087  efmival  12088  cos01gt0  12118  sin02gt0  12119  absefib  12126  efieq1re  12127  demoivre  12128  demoivreALT  12129  eirraplem  12132  0dvds  12166  odd2np1lem  12227  odd2np1  12228  even2n  12229  mod2eq0even  12233  2teven  12242  opoe  12250  omoe  12251  opeo  12252  omeo  12253  m1exp1  12256  bits0e  12304  bits0o  12305  bitsinv1  12317  gcd0id  12344  gcdid0  12345  1gcd  12357  lcmdvds  12445  isprm2lem  12482  isprm3  12484  prmgt1  12498  coprm  12510  isevengcd2  12524  isoddgcd1  12525  sqpweven  12541  2sqpwodd  12542  pythagtriplem12  12642  pythagtriplem13  12643  pythagtriplem14  12644  pythagtriplem16  12646  pc2dvds  12697  oddprmdvds  12721  pockthi  12725  1arith2  12735  unennn  12812  ctinfomlemom  12842  qnnen  12846  ssnnctlemct  12861  strslfv  12921  strle1g  12982  1strbas  12993  tgval  13138  ismgmn0  13234  mulgval  13502  mulgfng  13504  mulg0  13505  mulg1  13509  mulg2  13511  isnsg  13582  ringidvalg  13767  issrg  13771  subrgpropd  14059  rrgval  14068  islmod  14097  scaffvalg  14112  islssm  14163  sraval  14243  mopnset  14358  metuex  14361  zrhval  14423  zrhvalg  14424  zrhex  14427  psrbag  14475  istopon  14529  eltg4i  14571  eltg3  14573  tg1  14575  tg2  14576  topnex  14602  cldrcl  14618  restsn  14696  lmrcl  14707  metflem  14865  xmetf  14866  ismet2  14870  xmeteq0  14875  xmettri2  14877  xmetpsmet  14885  xmetres2  14895  blfvalps  14901  blex  14903  blvalps  14904  blval  14905  blfps  14925  blf  14926  mopnval  14958  cnbl0  15050  cnblcld  15051  blssioo  15069  resubmet  15072  cncfmet  15108  cnplimcim  15183  cnlimcim  15187  cnlimc  15188  dvfgg  15204  dvfpm  15205  dvfcnpm  15206  dvcj  15225  dvmptfsum  15241  reeff1olem  15287  ef2kpi  15322  sinperlem  15324  sin2kpi  15327  cos2kpi  15328  sinhalfpip  15336  sinhalfpim  15337  coshalfpip  15338  coshalfpim  15339  sincosq1sgn  15342  sinq12gt0  15346  sinkpi  15363  reeflog  15379  relogef  15380  logrpap0b  15392  loggt0b  15407  1cxp  15416  ecxp  15417  2logb9irrap  15493  0sgm  15501  lgsval2lem  15531  m1lgs  15606  1vgrex  15663  djucllem  15810  bdrabexg  15916  bdunexb  15930  peano5set  15950  speano5  15954  bj-omtrans  15966  pwf1oexmid  16010  nninfsellemeq  16025  iswomninnlem  16062