Theorem mpan 428

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 426	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  430  mpanl12  440  mp3an1  1365  mp3an12  1368  mp3an13  1369  ax9o  1750  sbnfc2  3208  ssdifss  3359  undifss  3608  uneqdifeqim  3613  elssuni  3961  csbexa  4260  difexg  4273  rabexg  4277  abssexg  4317  snexg  4319  copsexg  4382  sotritric  4467  sotritrieq  4468  trsuc  4565  oneli  4571  unexb  4586  opeluu  4594  rabxfr  4614  reuhyp  4616  ordunisuc2r  4659  reg3exmid  4725  brrelex12i  4815  brrelex1i  4816  brrelex2i  4817  xpss2  4884  opabid2  4909  eliunxp  4917  releldmi  5019  relelrni  5020  dmexg  5044  rnexg  5045  elres  5097  resexg  5101  relbrcnvg  5164  brcodir  5173  sotri  5181  sotri2  5183  sotri3  5184  dfrel2  5236  coi1  5301  fco  5550  fssres  5563  fabexg  5577  fvopab3g  5775  mptrcl  5785  mpteqb  5793  elfvmptrab1  5797  ffvelcdmi  5836  fsn2  5876  dfmptg  5882  fcof  5888  fvpr1  5913  fvconst2  5925  mptexg  5936  oprabid  6111  ovprc  6115  caovcl  6238  caovass  6244  caovdi  6263  elmpocl  6278  relmptopab  6285  ofexg  6301  resfunexgALT  6331  fo1stresm  6389  fo2ndresm  6390  1stexg  6395  2ndexg  6396  elopabi  6425  mpoexxg  6440  elmpom  6468  supp0  6472  mpoxopn0yelv  6504  rntpos  6522  smores  6557  tfr0dm  6587  tfrlemibxssdm  6592  tfrexlem  6599  tfr1onlembxssdm  6608  tfrcllembxssdm  6621  rdgruledefgg  6640  rdgruledefg  6641  rdgivallem  6646  rdgexg  6654  frec0g  6662  ordgt0ge1  6702  omfnex  6716  oeiv  6723  nna0r  6745  nnm0r  6746  nnsucsssuc  6759  nn2m  6794  nnaordex  6795  nnawordex  6796  ecdmn0m  6845  ecelqsi  6857  ecidg  6867  ectocl  6870  mapfset  6939  encv  7022  f1oen  7039  ssdomg  7059  map1  7095  fiprc  7098  dom1o  7110  xpdom1  7127  fict  7164  isinfinf  7195  ac6sfi  7196  xpfi  7233  en1eqsn  7259  fidcenumlemr  7266  fiss  7305  fipwfi  7315  eqinfti  7354  djueq2  7375  djulclr  7383  djurclr  7384  djulcl  7385  djurcl  7386  djuf1olem  7387  djulclb  7389  inl11  7399  eldju1st  7405  1stinl  7408  2ndinl  7409  1stinr  7410  2ndinr  7411  ctssdccl  7445  isomnimap  7471  ismkvmap  7488  iswomnimap  7500  finacn  7554  djucomen  7566  exmidapne  7620  0nnq  7725  mulidnq  7750  archnqq  7778  prarloclemarch2  7780  nqnq0pi  7799  nq0m0r  7817  nq02m  7826  prarloclemlt  7854  prarloclemn  7860  prarloclem5  7861  addnqprllem  7888  addnqprulem  7889  appdivnq  7924  1idprl  7951  1idpru  7952  addextpr  7982  cauappcvgprlemdisj  8012  cauappcvgprlemloc  8013  cauappcvgprlemladdru  8017  cauappcvgprlemladdrl  8018  caucvgprlemnbj  8028  caucvgprlemloc  8036  caucvgprprlemnbj  8054  caucvgprprlemloc  8064  caucvgprprlemaddq  8069  suplocexprlemmu  8079  suplocexprlemru  8080  suplocexprlemloc  8082  suplocexprlemlub  8085  0nsr  8110  ltsosr  8125  recexgt0sr  8134  prsrpos  8146  caucvgsr  8163  mappsrprg  8165  suplocsrlem  8169  mulresr  8199  axcnre  8242  axpre-ltwlin  8244  mullid  8318  0re  8320  axmulgt0  8391  ltnsym2  8410  eqlei  8413  ltnei  8423  muladd11  8453  cnegex  8498  0cnALT  8510  negcl  8520  negneg  8570  mul02  8708  mulm1  8721  lt0neg2  8791  le0neg2  8793  recexre  8900  recexgt0  8902  mulge0  8941  gt0ap0i  8949  recextlem1  8973  recexap  8975  recclapzi  9061  recap0apzi  9062  recidapzi  9063  divassapzi  9086  divmulapzi  9087  divdirapzi  9088  rerecclapzi  9100  ltp1  9168  recgt0i  9230  ltmul1i  9244  ltdiv1i  9245  ltmuldivi  9246  ltmul2i  9247  lemul1i  9248  lemul2i  9249  sup3exmid  9281  nngt1ne1  9322  nnrecre  9324  nn0ge0  9571  nn0addcl  9581  nn0mulcl  9582  zgt0ge1  9686  dfuzi  9739  eluzel2  9909  eluz2b1  9984  uz2m1nn  9988  elnn0dc  9994  elnndc  9995  nn01to3  10000  zq  10009  nnrecq  10028  rpge0  10050  rpreccl  10064  mnflt  10168  pnfnlt  10172  mnfle  10177  xrlelttr  10191  xrltletr  10192  xrletr  10193  xgepnf  10201  xlt0neg2  10224  xle0neg2  10226  xaddpnf2  10232  xaddmnf2  10234  xaddid2  10248  elioomnf  10353  ige3m2fz  10437  fzshftral  10498  ige2m1fz1  10499  1fv  10529  4fvwrd4  10530  rebtwn2zlemstep  10670  qbtwnxr  10675  btwnzge0  10718  zmodid2  10772  q2txmodxeq0  10804  frec2uzrand  10825  frecuzrdgtcl  10832  frecfzennn  10846  nn0ennn  10853  uzennn  10856  0exp  10994  sqgt0api  11045  subsq2  11067  qsqeqor  11070  bernneq  11081  faclbnd  11162  faclbnd2  11163  faclbnd3  11164  hashinfuni  11199  hashxp  11250  hashpwfi  11252  iswrdiz  11294  lsw0  11335  ccatlid  11357  s1leng  11375  s1fv  11377  s111  11382  pfx0g  11431  2shfti  11579  reim  11600  imcl  11602  crim  11606  caucvgre  11730  rennim  11751  resqrexlemdecn  11761  qabsor  11824  absimle  11833  sqrtthi  11868  sqrtcli  11869  sqrtgt0i  11870  sqrtmsqi  11871  sqrtsqi  11872  sqsqrti  11873  sqrtge0i  11874  absidi  11875  absnidi  11876  xrmaxiflemlub  11997  serclim0  12054  fsum2d  12185  fsumcnv  12187  fsumconst  12204  modfsummodlem1  12206  fsumabs  12215  binom11  12236  prodf1  12292  prodfclim1  12294  prodsnf  12342  fprod2d  12373  fprodcnv  12375  efzval  12433  eftlub  12440  efsep  12441  ef4p  12444  efgt1  12447  reef11  12449  sinf  12454  cosf  12455  efi4p  12467  sinneg  12476  cosneg  12477  efival  12482  efmival  12483  cos01gt0  12513  sin02gt0  12514  absefib  12521  efieq1re  12522  demoivre  12523  demoivreALT  12524  eirraplem  12527  0dvds  12561  odd2np1lem  12622  odd2np1  12623  even2n  12624  mod2eq0even  12628  2teven  12637  opoe  12645  omoe  12646  opeo  12647  omeo  12648  m1exp1  12651  bits0e  12699  bits0o  12700  bitsinv1  12712  gcd0id  12739  gcdid0  12740  1gcd  12752  lcmdvds  12840  isprm2lem  12877  isprm3  12879  prmgt1  12893  coprm  12905  isevengcd2  12919  isoddgcd1  12920  sqpweven  12936  2sqpwodd  12937  pythagtriplem12  13037  pythagtriplem13  13038  pythagtriplem14  13039  pythagtriplem16  13041  pc2dvds  13092  oddprmdvds  13116  pockthi  13120  1arith2  13130  unennn  13271  ctinfomlemom  13301  qnnen  13305  ssnnctlemct  13320  strslfv  13380  slotm  13398  strle1g  13443  1strbas  13454  tgval  13599  ismgmn0  13661  mulgval  13908  mulgfng  13910  mulg0  13911  mulg1  13915  mulg2  13917  isnsg  13988  mgpplusg  14205  mgpbas  14208  ringidvalg  14247  ringidval  14248  issrg  14252  subrgpropd  14544  rrgval  14553  islmod  14610  scaffvalg  14626  islssm  14677  sraval  14757  mopnset  14872  metuex  14875  zrhval  14935  zrhvalg  14936  zrhex  14939  asclfval  15004  psrbag  15036  psrbagaddclfi  15044  istopon  15097  eltg4i  15139  eltg3  15141  tg1  15143  tg2  15144  topnex  15170  cldrcl  15186  restsn  15264  lmrcl  15276  metflem  15433  xmetf  15434  ismet2  15438  xmeteq0  15443  xmettri2  15445  xmetpsmet  15453  xmetres2  15463  blfvalps  15469  blex  15471  blvalps  15472  blval  15473  blfps  15493  blf  15494  mopnval  15526  cnbl0  15618  cnblcld  15619  blssioo  15637  resubmet  15640  cncfmet  15676  cnplimcim  15751  cnlimcim  15755  cnlimc  15756  dvfgg  15772  dvfpm  15773  dvfcnpm  15774  dvcj  15793  dvmptfsum  15809  reeff1olem  15855  ef2kpi  15890  sinperlem  15892  sin2kpi  15895  cos2kpi  15896  sinhalfpip  15904  sinhalfpim  15905  coshalfpip  15906  coshalfpim  15907  sincosq1sgn  15910  sinq12gt0  15914  sinkpi  15931  reeflog  15947  relogef  15948  logrpap0b  15960  loggt0b  15975  1cxp  15985  ecxp  15986  2logb9irrap  16062  log2tlbndlog2  16065  log2ublem2  16067  0sgm  16082  lgsval2lem  16112  m1lgs  16187  1vgrex  16244  upgrfi  16326  umgredgnlp  16376  wlkop  16572  clwwlkn0  16632  djucllem  16811  bdrabexg  16915  bdunexb  16929  peano5set  16949  speano5  16953  bj-omtrans  16965  pw1ninf  17004  pwf1oexmid  17012  nninfsellemeq  17031  iswomninnlem  17073