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  1335  mp3an12  1338  mp3an13  1339  ax9o  1709  sbnfc2  3132  ssdifss  3280  undifss  3518  uneqdifeqim  3523  elssuni  3855  csbexa  4150  difexg  4162  rabexg  4164  abssexg  4203  snexg  4205  copsexg  4265  sotritric  4345  sotritrieq  4346  trsuc  4443  oneli  4449  unexb  4463  opeluu  4471  rabxfr  4491  reuhyp  4493  ordunisuc2r  4534  reg3exmid  4600  brrelex12i  4689  brrelex1i  4690  brrelex2i  4691  xpss2  4758  opabid2  4779  eliunxp  4787  releldmi  4887  relelrni  4888  dmexg  4912  rnexg  4913  elres  4964  resexg  4968  relbrcnvg  5028  brcodir  5037  sotri  5045  sotri2  5047  sotri3  5048  dfrel2  5100  coi1  5165  fco  5403  fssres  5413  fabexg  5425  fvopab3g  5613  mptrcl  5622  mpteqb  5630  elfvmptrab1  5634  ffvelcdmi  5674  fsn2  5714  dfmptg  5719  fvpr1  5744  fvconst2  5756  mptexg  5765  oprabid  5932  ovprc  5935  caovcl  6055  caovass  6061  caovdi  6080  elmpocl  6095  ofexg  6115  resfunexgALT  6137  fo1stresm  6190  fo2ndresm  6191  1stexg  6196  2ndexg  6197  elopabi  6224  mpoexxg  6239  mpoxopn0yelv  6268  rntpos  6286  smores  6321  tfr0dm  6351  tfrlemibxssdm  6356  tfrexlem  6363  tfr1onlembxssdm  6372  tfrcllembxssdm  6385  rdgruledefgg  6404  rdgruledefg  6405  rdgivallem  6410  rdgexg  6418  frec0g  6426  ordgt0ge1  6464  omfnex  6478  oeiv  6485  nna0r  6507  nnm0r  6508  nnsucsssuc  6521  nn2m  6556  nnaordex  6557  nnawordex  6558  ecdmn0m  6607  ecelqsi  6619  ecidg  6629  ectocl  6632  encv  6776  f1oen  6789  ssdomg  6808  map1  6842  fiprc  6845  xpdom1  6865  fict  6900  isinfinf  6929  ac6sfi  6930  xpfi  6962  en1eqsn  6981  fidcenumlemr  6988  fiss  7010  eqinfti  7053  djueq2  7074  djulclr  7082  djurclr  7083  djulcl  7084  djurcl  7085  djuf1olem  7086  djulclb  7088  inl11  7098  eldju1st  7104  1stinl  7107  2ndinl  7108  1stinr  7109  2ndinr  7110  ctssdccl  7144  isomnimap  7170  ismkvmap  7187  iswomnimap  7199  djucomen  7250  exmidapne  7294  0nnq  7398  mulidnq  7423  archnqq  7451  prarloclemarch2  7453  nqnq0pi  7472  nq0m0r  7490  nq02m  7499  prarloclemlt  7527  prarloclemn  7533  prarloclem5  7534  addnqprllem  7561  addnqprulem  7562  appdivnq  7597  1idprl  7624  1idpru  7625  addextpr  7655  cauappcvgprlemdisj  7685  cauappcvgprlemloc  7686  cauappcvgprlemladdru  7690  cauappcvgprlemladdrl  7691  caucvgprlemnbj  7701  caucvgprlemloc  7709  caucvgprprlemnbj  7727  caucvgprprlemloc  7737  caucvgprprlemaddq  7742  suplocexprlemmu  7752  suplocexprlemru  7753  suplocexprlemloc  7755  suplocexprlemlub  7758  0nsr  7783  ltsosr  7798  recexgt0sr  7807  prsrpos  7819  caucvgsr  7836  mappsrprg  7838  suplocsrlem  7842  mulresr  7872  axcnre  7915  axpre-ltwlin  7917  mullid  7990  0re  7992  axmulgt0  8064  ltnsym2  8083  eqlei  8086  ltnei  8096  muladd11  8125  cnegex  8170  0cnALT  8182  negcl  8192  negneg  8242  mul02  8379  mulm1  8392  lt0neg2  8461  le0neg2  8463  recexre  8570  recexgt0  8572  mulge0  8611  gt0ap0i  8619  recextlem1  8643  recexap  8645  recclapzi  8729  recap0apzi  8730  recidapzi  8731  divassapzi  8754  divmulapzi  8755  divdirapzi  8756  rerecclapzi  8768  ltp1  8836  recgt0i  8898  ltmul1i  8912  ltdiv1i  8913  ltmuldivi  8914  ltmul2i  8915  lemul1i  8916  lemul2i  8917  sup3exmid  8949  nngt1ne1  8989  nnrecre  8991  nn0ge0  9236  nn0addcl  9246  nn0mulcl  9247  zgt0ge1  9346  dfuzi  9398  eluzel2  9568  eluz2b1  9637  uz2m1nn  9641  elnn0dc  9647  elnndc  9648  nn01to3  9653  zq  9662  nnrecq  9681  rpge0  9702  rpreccl  9716  mnflt  9819  pnfnlt  9823  mnfle  9828  xrlelttr  9842  xrltletr  9843  xrletr  9844  xgepnf  9852  xlt0neg2  9875  xle0neg2  9877  xaddpnf2  9883  xaddmnf2  9885  xaddid2  9899  elioomnf  10004  ige3m2fz  10085  fzshftral  10144  ige2m1fz1  10145  1fv  10175  4fvwrd4  10176  rebtwn2zlemstep  10289  qbtwnxr  10294  btwnzge0  10337  zmodid2  10389  q2txmodxeq0  10421  frec2uzrand  10442  frecuzrdgtcl  10449  frecfzennn  10463  nn0ennn  10470  uzennn  10473  0exp  10595  sqgt0api  10646  subsq2  10668  qsqeqor  10671  bernneq  10681  faclbnd  10762  faclbnd2  10763  faclbnd3  10764  hashinfuni  10798  hashxp  10847  2shfti  10881  reim  10902  imcl  10904  crim  10908  caucvgre  11031  rennim  11052  resqrexlemdecn  11062  qabsor  11125  absimle  11134  sqrtthi  11169  sqrtcli  11170  sqrtgt0i  11171  sqrtmsqi  11172  sqrtsqi  11173  sqsqrti  11174  sqrtge0i  11175  absidi  11176  absnidi  11177  xrmaxiflemlub  11297  serclim0  11354  fsum2d  11484  fsumcnv  11486  fsumconst  11503  modfsummodlem1  11505  fsumabs  11514  binom11  11535  prodf1  11591  prodfclim1  11593  prodsnf  11641  fprod2d  11672  fprodcnv  11674  efzval  11732  eftlub  11739  efsep  11740  ef4p  11743  efgt1  11746  reef11  11748  sinf  11753  cosf  11754  efi4p  11766  sinneg  11775  cosneg  11776  efival  11781  efmival  11782  cos01gt0  11811  sin02gt0  11812  absefib  11819  efieq1re  11820  demoivre  11821  demoivreALT  11822  eirraplem  11825  0dvds  11859  odd2np1lem  11918  odd2np1  11919  even2n  11920  mod2eq0even  11924  2teven  11933  opoe  11941  omoe  11942  opeo  11943  omeo  11944  m1exp1  11947  gcd0id  12021  gcdid0  12022  1gcd  12034  lcmdvds  12122  isprm2lem  12159  isprm3  12161  prmgt1  12175  coprm  12187  isevengcd2  12201  isoddgcd1  12202  sqpweven  12218  2sqpwodd  12219  pythagtriplem12  12318  pythagtriplem13  12319  pythagtriplem14  12320  pythagtriplem16  12322  pc2dvds  12373  oddprmdvds  12397  pockthi  12401  1arith2  12411  unennn  12459  ctinfomlemom  12489  qnnen  12493  ssnnctlemct  12508  strslfv  12568  strle1g  12629  1strbas  12640  tgval  12778  ismgmn0  12845  mulgval  13087  mulgfng  13089  mulg0  13090  mulg1  13094  mulg2  13096  isnsg  13166  ringidvalg  13340  issrg  13344  subrgpropd  13620  islmod  13632  scaffvalg  13647  islssm  13698  sraval  13778  zrhvalg  13940  zrhex  13943  psrbag  13972  istopon  13998  eltg4i  14040  eltg3  14042  tg1  14044  tg2  14045  topnex  14071  cldrcl  14087  restsn  14165  lmrcl  14176  metflem  14334  xmetf  14335  ismet2  14339  xmeteq0  14344  xmettri2  14346  xmetpsmet  14354  xmetres2  14364  blfvalps  14370  blex  14372  blvalps  14373  blval  14374  blfps  14394  blf  14395  mopnval  14427  cnbl0  14519  cnblcld  14520  blssioo  14530  resubmet  14533  cncfmet  14564  cnplimcim  14621  cnlimcim  14625  cnlimc  14626  dvfgg  14642  dvfpm  14643  dvfcnpm  14644  dvcj  14658  reeff1olem  14677  ef2kpi  14712  sinperlem  14714  sin2kpi  14717  cos2kpi  14718  sinhalfpip  14726  sinhalfpim  14727  coshalfpip  14728  coshalfpim  14729  sincosq1sgn  14732  sinq12gt0  14736  sinkpi  14753  reeflog  14769  relogef  14770  logrpap0b  14782  loggt0b  14797  1cxp  14806  ecxp  14807  2logb9irrap  14880  lgsval2lem  14897  m1lgs  14938  djucllem  15038  bdrabexg  15144  bdunexb  15158  peano5set  15178  speano5  15182  bj-omtrans  15194  pwf1oexmid  15236  nninfsellemeq  15250  iswomninnlem  15285