Theorem mp2an 424

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 422	. 2 |- ( ps -> ch )
5	1, 4	ax-mp 5	1 |- ch

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:  mp4an  425  jaoi  711  mp3an  1332  barbara  2117  eqeq12i  2184  vtocl2  2785  spc2ev  2826  sbc2ie  3026  csbieb  3090  sseq12i  3175  uneq12i  3279  ineq12i  3326  ifssun  3540  nelpri  3607  ralpr  3638  rexpr  3639  preq12i  3665  dfop  3764  opeq12i  3770  breq12i  3998  mpteq2ia  4075  exmidundif  4192  exmidundifim  4193  opex  4214  opi2  4218  opth2  4225  opeqsn  4237  opeqpr  4238  uniop  4240  opelopaba  4251  braba  4252  opelopab  4256  brab  4257  opelopabaf  4258  unex  4426  snnex  4433  op1stb  4463  ifelpwun  4468  onun2i  4475  onsucssi  4490  ontriexmidim  4506  ontr2exmid  4509  onsucsssucexmid  4511  onsucelsucexmid  4514  opthreg  4540  tfis  4567  finds  4584  finds2  4585  nnregexmid  4605  xpeq12i  4633  opelvv  4661  eqrelriiv  4705  eqrelrdv  4707  xpss  4719  xpex  4726  relop  4761  brco  4782  opelcnv  4793  brcnv  4794  asymref  4996  codir  4999  ssrnres  5053  dmprop  5085  dfco2  5110  cossxp  5133  cocnvss  5136  coex  5156  funsn  5246  fnsn  5252  feq23i  5342  resasplitss  5377  fabex  5386  fvex  5516  xpsn  5672  fmptap  5686  opabex  5720  acexmidlemv  5851  oveq12i  5865  oprabid  5885  oprabss  5939  caovcom  6010  opabex3  6101  iunex  6102  oprabex  6107  ofmres  6115  op1st  6125  op2nd  6126  fo1st  6136  fo2nd  6137  mpoex  6193  1stconst  6200  2ndconst  6201  algrflem  6208  dftpos4  6242  tpostpos  6243  tpossym  6255  frecex  6373  frecfnom  6380  sucinc  6424  fnoei  6431  oeiexg  6432  nnacli  6461  nnmcli  6462  elec  6552  ecovcom  6620  ecovass  6622  ecovdi  6624  fnmap  6633  mapval  6638  elmap  6655  elpm  6657  elpm2  6658  map0  6667  ixpconst  6686  entri  6764  endisj  6802  xpcomco  6804  phplem2  6831  ssfiexmid  6854  domfiexmid  6856  unfiexmid  6895  unfiin  6903  inresflem  7037  casefun  7062  caserel  7064  caseinj  7066  omp1eomlem  7071  omp1eom  7072  endjusym  7073  djufun  7081  djuinj  7083  ctssdccl  7088  ctssdclemr  7089  nninfex  7098  infnninf  7100  fodjuomnilemdc  7120  ctssexmid  7126  exmidonfinlem  7170  dju1p1e2  7174  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidaclem  7185  pw1dom2  7204  onntri35  7214  onntri45  7218  1lt2pi  7302  indpi  7304  1nq  7328  rec1nq  7357  1lt2nq  7368  ltaddnq  7369  halfnqq  7372  prarloclemarch2  7381  prarloclemlt  7455  prarloclemcalc  7464  genpelxp  7473  ltexprlempr  7570  recexprlempr  7594  cauappcvgprlemcl  7615  cauappcvgprlemladd  7620  caucvgprlemcl  7638  caucvgprprlemcl  7666  suplocexprlemell  7675  suplocexprlemdisj  7682  suplocexprlemub  7685  0r  7712  1sr  7713  m1r  7714  m1p1sr  7722  m1m1sr  7723  0lt1sr  7727  1ne0sr  7728  1idsr  7730  recexgt0sr  7735  prsradd  7748  caucvgsrlemoffres  7762  caucvgsr  7764  mappsrprg  7766  map2psrprg  7767  pitonnlem1p1  7808  pitonnlem2  7809  pitoregt0  7811  peano2nnnn  7815  axi2m1  7837  axprecex  7842  axcnre  7843  nnindnn  7855  nntopi  7856  0cn  7912  addcli  7924  mulcli  7925  mulcomi  7926  readdcli  7933  remulcli  7934  rexpssxrxp  7964  ltrelxr  7980  gtneii  8015  lttri3i  8017  letri3i  8018  ltnsymi  8019  lenlti  8020  ltlei  8021  mulgt0i  8029  mulgt0ii  8030  0lt1  8046  addcomi  8063  pncan3oi  8135  resubcli  8182  subcli  8195  pncan3i  8196  negsubi  8197  subnegi  8198  subeq0i  8199  neg11i  8200  negcon1i  8201  negcon2i  8202  mulneg1i  8323  mulneg2i  8324  mul2negi  8325  addgt0ii  8410  ltnegi  8412  lenegi  8413  ltnegcon2i  8414  lesub0i  8415  ltaddposi  8416  posdifi  8417  ltnegcon1i  8418  lenegcon1i  8419  subge0i  8420  1ap0  8509  ltapii  8554  recrecapi  8661  dividapi  8662  div0api  8663  rec11apii  8678  divdiv32api  8684  recgt0ii  8823  ltrecii  8834  ltdiv23ii  8843  sup3exmid  8873  nnssre  8882  nnind  8894  nnmulcli  8900  nnsubi  8918  0le2  8968  1lt3  9049  2lt4  9051  1lt4  9052  3lt5  9054  2lt5  9055  1lt5  9056  4lt6  9058  3lt6  9059  2lt6  9060  1lt6  9061  5lt7  9063  4lt7  9064  3lt7  9065  2lt7  9066  1lt7  9067  6lt8  9069  5lt8  9070  4lt8  9071  3lt8  9072  2lt8  9073  1lt8  9074  7lt9  9076  6lt9  9077  5lt9  9078  4lt9  9079  3lt9  9080  2lt9  9081  1lt9  9082  2muline0  9103  nn0addcli  9172  nn0mulcli  9173  nn0addge1i  9183  nn0addge2i  9184  dfz2  9284  halfnz  9308  9p1e10  9345  numnncl  9352  numltc  9368  le9lt10  9369  nummac  9387  8lt10  9474  7lt10  9475  6lt10  9476  5lt10  9477  4lt10  9478  3lt10  9479  2lt10  9480  1lt10  9481  eluzaddi  9513  eluzsubi  9514  eluz2nn  9525  eluz4eluz2  9526  uzuzle23  9530  eluzge3nn  9531  divfnzn  9580  elq  9581  qreccl  9601  xrltnr  9736  mnfltpnf  9742  xaddmnf1  9805  pnfaddmnf  9807  mnfaddpnf  9808  xrex  9813  xaddid1  9819  xsubge0  9838  xposdif  9839  xleaddadd  9844  elicc2i  9896  ioomax  9905  iccmax  9906  ioopos  9907  elxrge0  9935  iccshftri  9952  iccshftli  9954  iccdili  9956  icccntri  9958  unitssre  9962  fz10  10002  fzpreddisj  10027  fz0to4untppr  10080  dfrp2  10220  fldiv4p1lem1div2  10261  frecfzennn  10382  fnn0nninf  10393  fxnn0nninf  10394  0tonninf  10395  1tonninf  10396  m1expcl2  10498  m1expcl  10499  nn0expcli  10502  sqmuli  10558  cu2  10574  i3  10577  subsqi  10585  binom2subi  10591  bcpasc  10700  4bc2eq6  10708  hashinfom  10712  prhash2ex  10744  hashp1i  10745  rei  10863  imi  10864  readdi  10892  imaddi  10893  remuli  10894  immuli  10895  cjaddi  10896  cjmuli  10897  ipcni  10898  crrei  10900  crimi  10901  rexfiuz  10953  sqrt1  11010  sqrt4  11011  sqrt9  11012  abs1  11036  sqrtmulii  11098  abslti  11102  abslei  11103  abssubi  11114  absmuli  11115  sqabsaddi  11116  sqabssubi  11117  abstrii  11119  fimaxre2  11190  climz  11255  abscn2  11278  recn2  11280  imcn2  11281  climabs  11283  climre  11285  climim  11286  fsumcnv  11400  fsumrelem  11434  fsumre  11435  fsumim  11436  arisum2  11462  expcnv  11467  geo2sum2  11478  geo2lim  11479  0.999...  11484  geoihalfsum  11485  fprodcnv  11588  fprodge0  11600  fprodge1  11602  ege2le3  11634  ef0  11635  reeff1  11663  tan0  11694  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  cos1bnd  11722  cos2bnd  11723  sin01gt0  11724  cos01gt0  11725  sin02gt0  11726  sincos1sgn  11727  sincos2sgn  11728  cos12dec  11730  egt2lt3  11742  epos  11743  ene1  11747  eap1  11748  3dvdsdec  11824  3dvds2dec  11825  odd2np1lem  11831  n2dvds1  11871  z4even  11875  ndvdsi  11892  flodddiv4  11893  gcd0val  11915  6gcd4e2  11950  3lcm2e6woprm  12040  6lcm4e12  12041  3lcm2e6  12114  sqrt2irrlem  12115  phimullem  12179  pockthi  12310  xpnnen  12349  xpomen  12350  ennnfonelemj0  12356  ennnfonelem0  12360  ennnfonelemhf1o  12368  exmidunben  12381  qnnen  12386  unct  12397  setscom  12456  strleun  12507  ismgm  12611  fn0g  12629  issgrp  12644  ismnddef  12654  txtopi  13055  txunii  13058  upxp  13066  uptx  13068  cnmpt1st  13082  cnmpt2nd  13083  txswaphmeolem  13114  qtopbasss  13315  cnmet  13324  cnopncntop  13331  remet  13334  blssioo  13339  tgqioo  13341  tgioo2cntop  13343  divcnap  13349  abscncf  13366  recncf  13367  imcncf  13368  cjcncf  13369  mulc1cncf  13370  cncfcn1cntop  13375  cdivcncfap  13381  expcncf  13386  cnrehmeocntop  13387  limccnp2lem  13439  limccnp2cntop  13440  dvcnp2cntop  13457  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465  dvrecap  13471  dveflem  13481  dvef  13482  sincn  13484  coscn  13485  reeff1oleme  13487  reeff1o  13488  cosz12  13495  sin0pilem1  13496  sin0pilem2  13497  pipos  13503  sinhalfpilem  13506  sincosq1lem  13540  sincosq1sgn  13541  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544  sinq12gt0  13545  cosq14gt0  13547  cosq23lt0  13548  coseq0q4123  13549  coseq00topi  13550  coseq0negpitopi  13551  tangtx  13553  sincos4thpi  13555  tan4thpi  13556  sincos6thpi  13557  pigt3  13559  cosordlem  13564  cosq34lt1  13565  cos02pilt1  13566  cos0pilt1  13567  ioocosf1o  13569  negpitopissre  13570  log1  13581  loge  13582  2logb9irr  13683  sqrt2cxp2logb9e3  13687  2logb9irrap  13689  lgsdir2lem2  13724  lgsdir2lem3  13725  2sqlem9  13754  2sqlem10  13755  ex-fl  13760  ex-ceil  13761  ex-bc  13764  ex-dvds  13765  ex-gcd  13766  bj-charfunbi  13846  bj-unex  13954  bj-nn0suc0  13985  bj-nntrans  13986  bj-nnelirr  13988  012of  14028  2o01f  14029  pwle2  14031  nnsf  14038  peano3nninf  14040  exmidsbthrlem  14054  sbthom  14058  isomninnlem  14062  iooref1o  14066  trilpolemisumle  14070  trilpolemeq1  14072  trilpolemlt1  14073  apdiff  14080  iswomninnlem  14081  iswomni0  14083  ismkvnnlem  14084  dceqnconst  14091  dcapnconst  14092  nconstwlpolemgt0  14095  taupi  14102