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  1360  mp3an12  1363  mp3an13  1364  ax9o  1745  sbnfc2  3187  ssdifss  3336  undifss  3574  uneqdifeqim  3579  elssuni  3922  csbexa  4219  difexg  4232  rabexg  4234  abssexg  4274  snexg  4276  copsexg  4338  sotritric  4423  sotritrieq  4424  trsuc  4521  oneli  4527  unexb  4541  opeluu  4549  rabxfr  4569  reuhyp  4571  ordunisuc2r  4614  reg3exmid  4680  brrelex12i  4770  brrelex1i  4771  brrelex2i  4772  xpss2  4839  opabid2  4863  eliunxp  4871  releldmi  4973  relelrni  4974  dmexg  4998  rnexg  4999  elres  5051  resexg  5055  relbrcnvg  5117  brcodir  5126  sotri  5134  sotri2  5136  sotri3  5137  dfrel2  5189  coi1  5254  fco  5502  fssres  5514  fabexg  5526  fvopab3g  5722  mptrcl  5732  mpteqb  5740  elfvmptrab1  5744  ffvelcdmi  5784  fsn2  5824  dfmptg  5830  fcof  5836  fvpr1  5861  fvconst2  5873  mptexg  5884  oprabid  6055  ovprc  6059  caovcl  6182  caovass  6188  caovdi  6207  elmpocl  6222  relmptopab  6229  ofexg  6245  resfunexgALT  6275  fo1stresm  6329  fo2ndresm  6330  1stexg  6335  2ndexg  6336  elopabi  6365  mpoexxg  6380  elmpom  6408  mpoxopn0yelv  6410  rntpos  6428  smores  6463  tfr0dm  6493  tfrlemibxssdm  6498  tfrexlem  6505  tfr1onlembxssdm  6514  tfrcllembxssdm  6527  rdgruledefgg  6546  rdgruledefg  6547  rdgivallem  6552  rdgexg  6560  frec0g  6568  ordgt0ge1  6608  omfnex  6622  oeiv  6629  nna0r  6651  nnm0r  6652  nnsucsssuc  6665  nn2m  6700  nnaordex  6701  nnawordex  6702  ecdmn0m  6751  ecelqsi  6763  ecidg  6773  ectocl  6776  encv  6920  f1oen  6937  ssdomg  6957  map1  6992  fiprc  6995  dom1o  7007  xpdom1  7024  fict  7060  isinfinf  7091  ac6sfi  7092  xpfi  7129  en1eqsn  7152  fidcenumlemr  7159  fiss  7181  eqinfti  7224  djueq2  7245  djulclr  7253  djurclr  7254  djulcl  7255  djurcl  7256  djuf1olem  7257  djulclb  7259  inl11  7269  eldju1st  7275  1stinl  7278  2ndinl  7279  1stinr  7280  2ndinr  7281  ctssdccl  7315  isomnimap  7341  ismkvmap  7358  iswomnimap  7370  finacn  7424  djucomen  7436  exmidapne  7484  0nnq  7589  mulidnq  7614  archnqq  7642  prarloclemarch2  7644  nqnq0pi  7663  nq0m0r  7681  nq02m  7690  prarloclemlt  7718  prarloclemn  7724  prarloclem5  7725  addnqprllem  7752  addnqprulem  7753  appdivnq  7788  1idprl  7815  1idpru  7816  addextpr  7846  cauappcvgprlemdisj  7876  cauappcvgprlemloc  7877  cauappcvgprlemladdru  7881  cauappcvgprlemladdrl  7882  caucvgprlemnbj  7892  caucvgprlemloc  7900  caucvgprprlemnbj  7918  caucvgprprlemloc  7928  caucvgprprlemaddq  7933  suplocexprlemmu  7943  suplocexprlemru  7944  suplocexprlemloc  7946  suplocexprlemlub  7949  0nsr  7974  ltsosr  7989  recexgt0sr  7998  prsrpos  8010  caucvgsr  8027  mappsrprg  8029  suplocsrlem  8033  mulresr  8063  axcnre  8106  axpre-ltwlin  8108  mullid  8182  0re  8184  axmulgt0  8256  ltnsym2  8275  eqlei  8278  ltnei  8288  muladd11  8317  cnegex  8362  0cnALT  8374  negcl  8384  negneg  8434  mul02  8571  mulm1  8584  lt0neg2  8654  le0neg2  8656  recexre  8763  recexgt0  8765  mulge0  8804  gt0ap0i  8812  recextlem1  8836  recexap  8838  recclapzi  8922  recap0apzi  8923  recidapzi  8924  divassapzi  8947  divmulapzi  8948  divdirapzi  8949  rerecclapzi  8961  ltp1  9029  recgt0i  9091  ltmul1i  9105  ltdiv1i  9106  ltmuldivi  9107  ltmul2i  9108  lemul1i  9109  lemul2i  9110  sup3exmid  9142  nngt1ne1  9183  nnrecre  9185  nn0ge0  9432  nn0addcl  9442  nn0mulcl  9443  zgt0ge1  9543  dfuzi  9595  eluzel2  9765  eluz2b1  9840  uz2m1nn  9844  elnn0dc  9850  elnndc  9851  nn01to3  9856  zq  9865  nnrecq  9884  rpge0  9906  rpreccl  9920  mnflt  10023  pnfnlt  10027  mnfle  10032  xrlelttr  10046  xrltletr  10047  xrletr  10048  xgepnf  10056  xlt0neg2  10079  xle0neg2  10081  xaddpnf2  10087  xaddmnf2  10089  xaddid2  10103  elioomnf  10208  ige3m2fz  10289  fzshftral  10348  ige2m1fz1  10349  1fv  10379  4fvwrd4  10380  rebtwn2zlemstep  10518  qbtwnxr  10523  btwnzge0  10566  zmodid2  10620  q2txmodxeq0  10652  frec2uzrand  10673  frecuzrdgtcl  10680  frecfzennn  10694  nn0ennn  10701  uzennn  10704  0exp  10842  sqgt0api  10893  subsq2  10915  qsqeqor  10918  bernneq  10928  faclbnd  11009  faclbnd2  11010  faclbnd3  11011  hashinfuni  11045  hashxp  11096  iswrdiz  11129  lsw0  11170  ccatlid  11192  s1leng  11210  s1fv  11212  s111  11217  pfx0g  11266  2shfti  11414  reim  11435  imcl  11437  crim  11441  caucvgre  11564  rennim  11585  resqrexlemdecn  11595  qabsor  11658  absimle  11667  sqrtthi  11702  sqrtcli  11703  sqrtgt0i  11704  sqrtmsqi  11705  sqrtsqi  11706  sqsqrti  11707  sqrtge0i  11708  absidi  11709  absnidi  11710  xrmaxiflemlub  11831  serclim0  11888  fsum2d  12019  fsumcnv  12021  fsumconst  12038  modfsummodlem1  12040  fsumabs  12049  binom11  12070  prodf1  12126  prodfclim1  12128  prodsnf  12176  fprod2d  12207  fprodcnv  12209  efzval  12267  eftlub  12274  efsep  12275  ef4p  12278  efgt1  12281  reef11  12283  sinf  12288  cosf  12289  efi4p  12301  sinneg  12310  cosneg  12311  efival  12316  efmival  12317  cos01gt0  12347  sin02gt0  12348  absefib  12355  efieq1re  12356  demoivre  12357  demoivreALT  12358  eirraplem  12361  0dvds  12395  odd2np1lem  12456  odd2np1  12457  even2n  12458  mod2eq0even  12462  2teven  12471  opoe  12479  omoe  12480  opeo  12481  omeo  12482  m1exp1  12485  bits0e  12533  bits0o  12534  bitsinv1  12546  gcd0id  12573  gcdid0  12574  1gcd  12586  lcmdvds  12674  isprm2lem  12711  isprm3  12713  prmgt1  12727  coprm  12739  isevengcd2  12753  isoddgcd1  12754  sqpweven  12770  2sqpwodd  12771  pythagtriplem12  12871  pythagtriplem13  12872  pythagtriplem14  12873  pythagtriplem16  12875  pc2dvds  12926  oddprmdvds  12950  pockthi  12954  1arith2  12964  unennn  13041  ctinfomlemom  13071  qnnen  13075  ssnnctlemct  13090  strslfv  13150  strle1g  13212  1strbas  13223  tgval  13368  ismgmn0  13464  mulgval  13732  mulgfng  13734  mulg0  13735  mulg1  13739  mulg2  13741  isnsg  13812  ringidvalg  13998  issrg  14002  subrgpropd  14291  rrgval  14300  islmod  14329  scaffvalg  14344  islssm  14395  sraval  14475  mopnset  14590  metuex  14593  zrhval  14655  zrhvalg  14656  zrhex  14659  psrbag  14707  istopon  14766  eltg4i  14808  eltg3  14810  tg1  14812  tg2  14813  topnex  14839  cldrcl  14855  restsn  14933  lmrcl  14945  metflem  15102  xmetf  15103  ismet2  15107  xmeteq0  15112  xmettri2  15114  xmetpsmet  15122  xmetres2  15132  blfvalps  15138  blex  15140  blvalps  15141  blval  15142  blfps  15162  blf  15163  mopnval  15195  cnbl0  15287  cnblcld  15288  blssioo  15306  resubmet  15309  cncfmet  15345  cnplimcim  15420  cnlimcim  15424  cnlimc  15425  dvfgg  15441  dvfpm  15442  dvfcnpm  15443  dvcj  15462  dvmptfsum  15478  reeff1olem  15524  ef2kpi  15559  sinperlem  15561  sin2kpi  15564  cos2kpi  15565  sinhalfpip  15573  sinhalfpim  15574  coshalfpip  15575  coshalfpim  15576  sincosq1sgn  15579  sinq12gt0  15583  sinkpi  15600  reeflog  15616  relogef  15617  logrpap0b  15629  loggt0b  15644  1cxp  15653  ecxp  15654  2logb9irrap  15730  0sgm  15738  lgsval2lem  15768  m1lgs  15843  1vgrex  15900  upgrfi  15982  umgredgnlp  16032  wlkop  16228  clwwlkn0  16288  djucllem  16457  bdrabexg  16561  bdunexb  16575  peano5set  16595  speano5  16599  bj-omtrans  16611  pw1ninf  16650  pwf1oexmid  16660  nninfsellemeq  16679  iswomninnlem  16721