Theorem mpan 420

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  mp2an  422  mpanl12  432  mp3an1  1302  mp3an12  1305  mp3an13  1306  ax9o  1676  sbnfc2  3060  ssdifss  3206  undifss  3443  uneqdifeqim  3448  elssuni  3764  csbexa  4057  difexg  4069  rabexg  4071  abssexg  4106  snexg  4108  copsexg  4166  sotritric  4246  sotritrieq  4247  trsuc  4344  oneli  4350  unexb  4363  opeluu  4371  rabxfr  4391  reuhyp  4393  ordunisuc2r  4430  reg3exmid  4494  brrelex12i  4581  brrelex1i  4582  brrelex2i  4583  xpss2  4650  opabid2  4670  eliunxp  4678  releldmi  4778  relelrni  4779  dmexg  4803  rnexg  4804  elres  4855  resexg  4859  relbrcnvg  4918  brcodir  4926  sotri  4934  sotri2  4936  sotri3  4937  dfrel2  4989  coi1  5054  fco  5288  fssres  5298  fabexg  5310  fvopab3g  5494  mptrcl  5503  mpteqb  5511  elfvmptrab1  5515  ffvelrni  5554  fsn2  5594  dfmptg  5599  fvpr1  5624  fvconst2  5636  mptexg  5645  oprabid  5803  ovprc  5806  caovcl  5925  caovass  5931  caovdi  5950  elmpocl  5968  ofexg  5986  resfunexgALT  6008  fo1stresm  6059  fo2ndresm  6060  1stexg  6065  2ndexg  6066  elopabi  6093  mpoexxg  6108  mpoxopn0yelv  6136  rntpos  6154  smores  6189  tfr0dm  6219  tfrlemibxssdm  6224  tfrexlem  6231  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  rdgruledefgg  6272  rdgruledefg  6273  rdgivallem  6278  rdgexg  6286  frec0g  6294  ordgt0ge1  6332  omfnex  6345  oeiv  6352  nna0r  6374  nnm0r  6375  nnsucsssuc  6388  nn2m  6422  nnaordex  6423  nnawordex  6424  ecdmn0m  6471  ecelqsi  6483  ecidg  6493  ectocl  6496  encv  6640  f1oen  6653  ssdomg  6672  map1  6706  fiprc  6709  xpdom1  6729  fict  6762  isinfinf  6791  ac6sfi  6792  xpfi  6818  en1eqsn  6836  fidcenumlemr  6843  fiss  6865  eqinfti  6907  djueq2  6926  djulclr  6934  djurclr  6935  djulcl  6936  djurcl  6937  djuf1olem  6938  djulclb  6940  inl11  6950  eldju1st  6956  1stinl  6959  2ndinl  6960  1stinr  6961  2ndinr  6962  ctssdccl  6996  isomnimap  7009  ismkvmap  7028  djucomen  7072  0nnq  7172  mulidnq  7197  archnqq  7225  prarloclemarch2  7227  nqnq0pi  7246  nq0m0r  7264  nq02m  7273  prarloclemlt  7301  prarloclemn  7307  prarloclem5  7308  addnqprllem  7335  addnqprulem  7336  appdivnq  7371  1idprl  7398  1idpru  7399  addextpr  7429  cauappcvgprlemdisj  7459  cauappcvgprlemloc  7460  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  caucvgprlemnbj  7475  caucvgprlemloc  7483  caucvgprprlemnbj  7501  caucvgprprlemloc  7511  caucvgprprlemaddq  7516  suplocexprlemmu  7526  suplocexprlemru  7527  suplocexprlemloc  7529  suplocexprlemlub  7532  0nsr  7557  ltsosr  7572  recexgt0sr  7581  prsrpos  7593  caucvgsr  7610  mappsrprg  7612  suplocsrlem  7616  mulresr  7646  axcnre  7689  axpre-ltwlin  7691  mulid2  7764  0re  7766  axmulgt0  7836  ltnsym2  7854  eqlei  7857  ltnei  7867  muladd11  7895  cnegex  7940  0cnALT  7952  negcl  7962  negneg  8012  mul02  8149  mulm1  8162  lt0neg2  8231  le0neg2  8233  recexre  8340  recexgt0  8342  mulge0  8381  gt0ap0i  8389  recextlem1  8412  recexap  8414  recclapzi  8497  recap0apzi  8498  recidapzi  8499  divassapzi  8522  divmulapzi  8523  divdirapzi  8524  rerecclapzi  8536  ltp1  8602  recgt0i  8664  ltmul1i  8678  ltdiv1i  8679  ltmuldivi  8680  ltmul2i  8681  lemul1i  8682  lemul2i  8683  sup3exmid  8715  nngt1ne1  8755  nnrecre  8757  nn0ge0  9002  nn0addcl  9012  nn0mulcl  9013  zgt0ge1  9112  dfuzi  9161  eluzel2  9331  eluz2b1  9395  uz2m1nn  9399  nn01to3  9409  zq  9418  nnrecq  9437  rpge0  9454  rpreccl  9468  mnflt  9569  pnfnlt  9573  mnfle  9578  xrlelttr  9589  xrltletr  9590  xrletr  9591  xgepnf  9599  xlt0neg2  9622  xle0neg2  9624  xaddpnf2  9630  xaddmnf2  9632  xaddid2  9646  elioomnf  9751  ige3m2fz  9829  fzshftral  9888  ige2m1fz1  9889  1fv  9916  4fvwrd4  9917  rebtwn2zlemstep  10030  qbtwnxr  10035  btwnzge0  10073  zmodid2  10125  q2txmodxeq0  10157  frec2uzrand  10178  frecuzrdgtcl  10185  frecfzennn  10199  nn0ennn  10206  uzennn  10209  0exp  10328  sqgt0api  10378  subsq2  10400  bernneq  10412  faclbnd  10487  faclbnd2  10488  faclbnd3  10489  hashinfuni  10523  hashxp  10572  2shfti  10603  reim  10624  imcl  10626  crim  10630  caucvgre  10753  rennim  10774  resqrexlemdecn  10784  qabsor  10847  absimle  10856  sqrtthi  10891  sqrtcli  10892  sqrtgt0i  10893  sqrtmsqi  10894  sqrtsqi  10895  sqsqrti  10896  sqrtge0i  10897  absidi  10898  absnidi  10899  xrmaxiflemlub  11017  serclim0  11074  fsum2d  11204  fsumcnv  11206  fsumconst  11223  modfsummodlem1  11225  fsumabs  11234  binom11  11255  prodf1  11311  prodfclim1  11313  efzval  11389  eftlub  11396  efsep  11397  ef4p  11400  efgt1  11403  reef11  11406  sinf  11411  cosf  11412  efi4p  11424  sinneg  11433  cosneg  11434  efival  11439  efmival  11440  cos01gt0  11469  sin02gt0  11470  absefib  11477  efieq1re  11478  demoivre  11479  demoivreALT  11480  eirraplem  11483  0dvds  11513  odd2np1lem  11569  odd2np1  11570  even2n  11571  mod2eq0even  11575  2teven  11584  opoe  11592  omoe  11593  opeo  11594  omeo  11595  m1exp1  11598  gcd0id  11667  gcdid0  11668  1gcd  11680  lcmdvds  11760  isprm2lem  11797  isprm3  11799  prmgt1  11812  coprm  11822  isevengcd2  11836  isoddgcd1  11837  sqpweven  11853  2sqpwodd  11854  unennn  11910  ctinfomlemom  11940  qnnen  11944  strslfv  12003  strle1g  12049  1strbas  12058  istopon  12180  tgval  12218  eltg4i  12224  eltg3  12226  tg1  12228  tg2  12229  topnex  12255  cldrcl  12271  restsn  12349  lmrcl  12360  metflem  12518  xmetf  12519  ismet2  12523  xmeteq0  12528  xmettri2  12530  xmetpsmet  12538  xmetres2  12548  blfvalps  12554  blex  12556  blvalps  12557  blval  12558  blfps  12578  blf  12579  mopnval  12611  cnbl0  12703  cnblcld  12704  blssioo  12714  resubmet  12717  cncfmet  12748  cnplimcim  12805  cnlimcim  12809  cnlimc  12810  dvfgg  12826  dvfpm  12827  dvfcnpm  12828  dvcj  12842  ef2kpi  12887  sinperlem  12889  sin2kpi  12892  cos2kpi  12893  sinhalfpip  12901  sinhalfpim  12902  coshalfpip  12903  coshalfpim  12904  sincosq1sgn  12907  sinq12gt0  12911  sinkpi  12928  djucllem  13007  bdrabexg  13104  bdunexb  13118  peano5set  13138  speano5  13142  bj-omtrans  13154  pwf1oexmid  13194  nninfsellemeq  13210