Theorem mp2an 430

Description: An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)

Hypotheses

Ref	Expression
mp2an.1	|- ph
mp2an.2	|- ps
mp2an.3	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
mp2an	|- ch

Proof of Theorem mp2an

Step	Hyp	Ref	Expression
1		mp2an.2	. 2 |- ps
2		mp2an.1	. . 3 |- ph
3		mp2an.3	. . 3 |- ( ( ph /\ ps ) -> ch )
4	2, 3	mpan 428	. 2 |- ( ps -> ch )
5	1, 4	ax-mp 5	1 |- ch

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:  mp4an  431  jaoi  728  mp3an  1378  barbara  2185  eqeq12i  2252  el2v  2827  vtocl2  2878  spc2ev  2921  sbc2ie  3123  csbieb  3189  sseq12i  3276  uneq12i  3381  ineq12i  3430  ifssun  3652  nelpri  3729  ralpr  3760  rexpr  3761  preq12i  3789  dfop  3898  opeq12i  3904  breq12i  4134  mpteq2ia  4212  exmidundif  4338  exmidundifim  4339  opex  4364  opi2  4368  opth2  4375  opeqsn  4388  opeqpr  4389  uniop  4391  opelopaba  4403  braba  4404  opelopab  4409  brab  4410  opelopabaf  4411  unex  4582  snnex  4589  op1stb  4619  ifelpwun  4624  ifex  4627  onun2i  4633  onsucssi  4648  ontriexmidim  4664  ontr2exmid  4667  onsucsssucexmid  4669  onsucelsucexmid  4672  opthreg  4698  tfis  4725  finds  4742  finds2  4743  nnregexmid  4763  xpeq12i  4791  opelvv  4820  eqrelriiv  4864  eqrelrdv  4866  xpss  4878  xpex  4886  relop  4925  brco  4946  opelcnv  4957  brcnv  4958  asymref  5168  codir  5171  ssrnres  5225  dmprop  5257  dfco2  5282  cossxp  5305  cocnvss  5308  coex  5328  funsn  5424  fnsn  5430  feq23i  5523  resasplitss  5564  fabex  5575  fvex  5710  xpsn  5876  fmptap  5896  opabex  5932  rinvf1o  6025  acexmidlemv  6073  oveq12i  6087  oprabid  6107  oprabss  6164  caovcom  6237  opabex3  6341  iunex  6342  oprabex  6351  ofmres  6359  op1st  6370  op2nd  6371  fo1st  6381  fo2nd  6382  mpoex  6440  1stconst  6447  2ndconst  6448  algrflem  6455  dftpos4  6524  tpostpos  6525  tpossym  6537  frecex  6655  frecfnom  6662  2oex  6694  sucinc  6708  fnoei  6715  oeiexg  6716  nnacli  6745  nnmcli  6746  elec  6838  ecovcom  6906  ecovass  6908  ecovdi  6910  fnmap  6919  mapval  6924  elmap  6948  elpm  6950  elpm2  6951  map0  6961  ixpconst  6980  entri  7063  endisj  7112  xpcomco  7114  phplem2  7144  1ndom2  7156  ssfiexmid  7168  domfiexmid  7172  exmidpw2en  7209  unfiexmid  7215  unfiin  7223  inresflem  7390  casefun  7415  caserel  7417  caseinj  7419  omp1eomlem  7424  omp1eom  7425  endjusym  7426  djufun  7434  djuinj  7436  ctssdccl  7441  ctssdclemr  7442  nninfex  7451  infnninf  7454  fodjuomnilemdc  7474  ctssexmid  7480  exmidonfinlem  7535  dju1p1e2  7539  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  exmidaclem  7554  pw1dom2  7576  onntri35  7586  onntri45  7590  2oneel  7612  2omotaplemst  7614  acnccim  7628  1lt2pi  7697  indpi  7699  1nq  7723  rec1nq  7752  1lt2nq  7763  ltaddnq  7764  halfnqq  7767  prarloclemarch2  7776  prarloclemlt  7850  prarloclemcalc  7859  genpelxp  7868  ltexprlempr  7965  recexprlempr  7989  cauappcvgprlemcl  8010  cauappcvgprlemladd  8015  caucvgprlemcl  8033  caucvgprprlemcl  8061  suplocexprlemell  8070  suplocexprlemdisj  8077  suplocexprlemub  8080  0r  8107  1sr  8108  m1r  8109  m1p1sr  8117  m1m1sr  8118  0lt1sr  8122  1ne0sr  8123  1idsr  8125  recexgt0sr  8130  prsradd  8143  caucvgsrlemoffres  8157  caucvgsr  8159  mappsrprg  8161  map2psrprg  8162  pitonnlem1p1  8203  pitonnlem2  8204  pitoregt0  8206  peano2nnnn  8210  axi2m1  8232  axprecex  8237  axcnre  8238  nnindnn  8250  nntopi  8251  0cn  8308  addcli  8320  mulcli  8321  mulcomi  8322  readdcli  8329  remulcli  8330  rexpssxrxp  8360  ltrelxr  8376  gtneii  8411  lttri3i  8413  letri3i  8414  ltnsymi  8415  lenlti  8416  ltlei  8417  mulgt0i  8425  mulgt0ii  8426  0lt1  8443  addcomi  8460  pncan3oi  8532  resubcli  8579  subcli  8592  pncan3i  8593  negsubi  8594  subnegi  8595  subeq0i  8596  neg11i  8597  negcon1i  8598  negcon2i  8599  mulneg1i  8721  mulneg2i  8722  mul2negi  8723  addgt0ii  8809  ltnegi  8811  lenegi  8812  ltnegcon2i  8813  lesub0i  8814  ltaddposi  8815  posdifi  8816  ltnegcon1i  8817  lenegcon1i  8818  subge0i  8819  1ap0  8908  ltapii  8953  recrecapi  9064  dividapi  9065  div0api  9066  rec11apii  9081  divdiv32api  9087  recgt0ii  9227  ltrecii  9238  ltdiv23ii  9247  sup3exmid  9277  nnssre  9287  nnind  9299  nnmulcli  9305  nnsubi  9323  0le2  9373  1lt3  9455  2lt4  9457  1lt4  9458  3lt5  9460  2lt5  9461  1lt5  9462  4lt6  9464  3lt6  9465  2lt6  9466  1lt6  9467  5lt7  9469  4lt7  9470  3lt7  9471  2lt7  9472  1lt7  9473  6lt8  9475  5lt8  9476  4lt8  9477  3lt8  9478  2lt8  9479  1lt8  9480  7lt9  9482  6lt9  9483  5lt9  9484  4lt9  9485  3lt9  9486  2lt9  9487  1lt9  9488  2muline0  9509  nn0addcli  9579  nn0mulcli  9580  nn0addge1i  9590  nn0addge2i  9591  dfz2  9696  halfnz  9721  9p1e10  9758  numnncl  9765  numltc  9781  le9lt10  9782  nummac  9800  8lt10  9887  7lt10  9888  6lt10  9889  5lt10  9890  4lt10  9891  3lt10  9892  2lt10  9893  1lt10  9894  eluzaddi  9928  eluzsubi  9929  uzuzle23  9941  uzuzle24  9942  uzuzle34  9943  eluz2nn  9945  eluz4eluz2  9947  eluzge3nn  9951  divfnzn  10000  elq  10001  qreccl  10021  xrltnr  10160  mnfltpnf  10166  xaddmnf1  10229  pnfaddmnf  10231  mnfaddpnf  10232  xrex  10237  xaddid1  10243  xsubge0  10262  xposdif  10263  xleaddadd  10268  elicc2i  10320  ioomax  10329  iccmax  10330  ioopos  10331  elxrge0  10359  iccshftri  10376  iccshftli  10378  iccdili  10380  icccntri  10382  unitssre  10387  fz10  10429  fzpreddisj  10456  fz0to4untppr  10509  dfrp2  10676  fldiv4p1lem1div2  10718  fldiv4lem1div2  10720  frecfzennn  10841  xnn0nnen  10852  fnn0nninf  10853  fxnn0nninf  10854  0tonninf  10855  1tonninf  10856  m1expcl2  10976  m1expcl  10977  nn0expcli  10980  sqmuli  11037  cu2  11053  i3  11056  subsqi  11064  binom2subi  11070  bcpasc  11182  4bc2eq6  11191  hashinfom  11195  prhash2ex  11228  hashp1i  11229  lsw0g  11331  swrdccat3blem  11489  rei  11643  imi  11644  readdi  11672  imaddi  11673  remuli  11674  immuli  11675  cjaddi  11676  cjmuli  11677  ipcni  11678  crrei  11680  crimi  11681  rexfiuz  11733  sqrt1  11790  sqrt4  11791  sqrt9  11792  abs1  11816  sqrtmulii  11878  abslti  11882  abslei  11883  abssubi  11894  absmuli  11895  sqabsaddi  11896  sqabssubi  11897  abstrii  11899  fimaxre2  11971  climz  12036  abscn2  12059  recn2  12061  imcn2  12062  climabs  12064  climre  12066  climim  12067  fsumcnv  12182  fsumrelem  12216  fsumre  12217  fsumim  12218  arisum2  12244  expcnv  12249  geo2sum2  12260  geo2lim  12261  0.999...  12266  geoihalfsum  12267  fprodcnv  12370  fprodge0  12382  fprodge1  12384  ege2le3  12416  ef0  12417  reeff1  12445  tan0  12476  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  cos1bnd  12504  cos2bnd  12505  sinltxirr  12506  sin01gt0  12507  cos01gt0  12508  sin02gt0  12509  sincos1sgn  12510  sincos2sgn  12511  cos12dec  12513  egt2lt3  12525  epos  12526  ene1  12530  eap1  12531  3dvds  12609  3dvdsdec  12610  3dvds2dec  12611  odd2np1lem  12617  n2dvds1  12657  z4even  12661  ndvdsi  12678  flodddiv4  12681  bitsp1o  12698  0bits  12704  gcd0val  12715  6gcd4e2  12750  3lcm2e6woprm  12842  6lcm4e12  12843  3lcm2e6  12916  sqrt2irrlem  12917  phimullem  12981  pockthi  13115  4sqlem19  13166  dec2dvds  13168  dec5dvds2  13170  dec2nprm  13172  modxai  13173  gcdi  13177  gcdmodi  13178  numexpp1  13181  karatsuba  13187  2exp7  13191  ballotfilemofi  13197  ballotfilem1  13198  ballotfilem2  13206  ballotfilemfmpn  13212  ballotfilemefi  13215  ballotfilemodife  13218  ballotfilem4  13219  ballotfilemiex  13222  ballotfilemimin  13227  ballotfilemic  13228  ballotfilemsval  13230  ballotfilemsdom  13233  ballotfilemsel1i  13234  ballotfilemsima  13237  ballotfilemrval  13239  ballotfilemfrceq  13250  ballotfilemfrcn0  13251  ballotfilem1ri  13256  ballotfilem7  13257  ballotfilem8  13258  ballotfilemth  13259  xpnnen  13263  xpomen  13264  ennnfonelemj0  13270  ennnfonelem0  13274  ennnfonelemhf1o  13282  exmidunben  13295  qnnen  13300  unct  13311  setscom  13370  strleun  13435  prdsvallem  13598  imasival  13604  ismgm  13654  fn0g  13672  fngzsum  13685  issgrp  13695  ismnddef  13708  isghm  14023  prdsex  14149  isrng  14208  rngmgpf  14211  isring  14278  mgpf  14289  dfrhm2  14434  rhmex  14437  isdomn  14551  rmodislmod  14660  lidlmex  14784  mopnset  14861  cnfldstr  14867  cnfldcj  14874  cnfld0  14880  cnfldplusf  14883  zringcrng  14899  zringmulr  14906  zringmpg  14913  znval  14943  psrval  14973  fnpsr  14974  fnmpl  15007  txtopi  15285  txunii  15288  upxp  15296  uptx  15298  cnmpt1st  15312  cnmpt2nd  15313  txswaphmeolem  15344  qtopbasss  15545  cnmet  15554  cnfldms  15560  cnopncntop  15568  cnopn  15569  remet  15572  blssioo  15577  tgqioo  15579  tgioo2cntop  15581  tgioo2  15583  divcnap  15589  abscncf  15609  recncf  15610  imcncf  15611  cjcncf  15612  mulc1cncf  15613  cncfcn1cntop  15618  idcncf  15625  cdivcncfap  15628  expcncf  15633  cnrehmeocntop  15634  maxcncf  15639  mincncf  15640  ivthreinc  15669  hovercncf  15670  limccnp2lem  15700  limccnp2cntop  15701  dvcnp2cntop  15723  dvaddxxbr  15725  dvmulxxbr  15726  dvcoapbr  15731  dvrecap  15737  dveflem  15750  dvef  15751  sincn  15793  coscn  15794  reeff1oleme  15796  reeff1o  15797  cosz12  15804  sin0pilem1  15805  sin0pilem2  15806  pipos  15812  sinhalfpilem  15815  sincosq1lem  15849  sincosq1sgn  15850  sincosq2sgn  15851  sincosq3sgn  15852  sincosq4sgn  15853  sinq12gt0  15854  cosq14gt0  15856  cosq23lt0  15857  coseq0q4123  15858  coseq00topi  15859  coseq0negpitopi  15860  tangtx  15862  sincos4thpi  15864  tan4thpi  15865  sincos6thpi  15866  pigt3  15868  cosordlem  15873  cosq34lt1  15874  cos02pilt1  15875  cos0pilt1  15876  ioocosf1o  15878  negpitopissre  15879  log1  15890  loge  15891  2logb9irr  15996  sqrt2cxp2logb9e3  16000  2logb9irrap  16002  mpodvdsmulf1o  16018  fsumdvdsmul  16019  1sgm2ppw  16023  lgsdir2lem2  16062  lgsdir2lem3  16063  lgseisenlem4  16106  2lgsoddprmlem3  16144  2sqlem9  16157  2sqlem10  16158  opvtxfvi  16182  opiedgfvi  16183  umgrbien  16265  usgrprc  16407  vtxdfifiun  16452  upgr2wlkdc  16532  konigsbergvtx  16637  konigsbergiedg  16638  konigsbergumgr  16642  konigsberglem1  16643  konigsberglem2  16644  konigsberglem3  16645  konigsberglem5  16647  konigsberg  16648  ex-fl  16653  ex-ceil  16654  ex-bc  16657  ex-dvds  16658  ex-gcd  16659  bj-charfunbi  16751  bj-unex  16859  bj-nn0suc0  16890  bj-nntrans  16891  bj-nnelirr  16893  012of  16937  2o01f  16938  pwle2  16942  nnsf  16953  peano3nninf  16955  exmidsbthrlem  16972  sbthom  16976  repiecelem  16979  repiecele0  16980  repiecege0  16981  isomninnlem  16984  iooref1o  16988  trilpolemisumle  16992  trilpolemeq1  16994  trilpolemlt1  16995  apdiff  17002  iswomninnlem  17004  iswomni0  17006  ismkvnnlem  17007  dceqnconst  17015  dcapnconst  17016  nconstwlpolemgt0  17019  taupi  17028