Theorem mp2an 423

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 421	. 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  424  jaoi  706  mp3an  1316  barbara  2098  eqeq12i  2154  vtocl2  2744  spc2ev  2785  sbc2ie  2984  csbieb  3046  sseq12i  3130  uneq12i  3233  ineq12i  3280  nelpri  3556  ralpr  3586  rexpr  3587  preq12i  3613  dfop  3712  opeq12i  3718  breq12i  3946  mpteq2ia  4022  exmidundif  4137  exmidundifim  4138  opex  4159  opi2  4163  opth2  4170  opeqsn  4182  opeqpr  4183  uniop  4185  opelopaba  4196  braba  4197  opelopab  4201  brab  4202  opelopabaf  4203  unex  4370  snnex  4377  op1stb  4407  onun2i  4415  onsucssi  4430  ontr2exmid  4448  onsucsssucexmid  4450  onsucelsucexmid  4453  opthreg  4479  tfis  4505  finds  4522  finds2  4523  nnregexmid  4542  xpeq12i  4569  opelvv  4597  eqrelriiv  4641  eqrelrdv  4643  xpss  4655  xpex  4662  relop  4697  brco  4718  opelcnv  4729  brcnv  4730  asymref  4932  codir  4935  ssrnres  4989  dmprop  5021  dfco2  5046  cossxp  5069  cocnvss  5072  coex  5092  funsn  5179  fnsn  5185  feq23i  5275  resasplitss  5310  fabex  5319  fvex  5449  xpsn  5604  fmptap  5618  opabex  5652  acexmidlemv  5780  oveq12i  5794  oprabid  5811  oprabss  5865  caovcom  5936  opabex3  6028  iunex  6029  oprabex  6034  ofmres  6042  op1st  6052  op2nd  6053  fo1st  6063  fo2nd  6064  mpoex  6119  1stconst  6126  2ndconst  6127  algrflem  6134  dftpos4  6168  tpostpos  6169  tpossym  6181  frecex  6299  frecfnom  6306  sucinc  6349  fnoei  6356  oeiexg  6357  nnacli  6386  nnmcli  6387  elec  6476  ecovcom  6544  ecovass  6546  ecovdi  6548  fnmap  6557  mapval  6562  elmap  6579  elpm  6581  elpm2  6582  map0  6591  ixpconst  6610  entri  6688  endisj  6726  xpcomco  6728  phplem2  6755  ssfiexmid  6778  domfiexmid  6780  unfiexmid  6814  unfiin  6822  inresflem  6953  casefun  6978  caserel  6980  caseinj  6982  omp1eomlem  6987  omp1eom  6988  endjusym  6989  djufun  6997  djuinj  6999  ctssdccl  7004  ctssdclemr  7005  fodjuomnilemdc  7024  ctssexmid  7032  exmidonfinlem  7066  dju1p1e2  7070  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  exmidaclem  7081  1lt2pi  7172  indpi  7174  1nq  7198  rec1nq  7227  1lt2nq  7238  ltaddnq  7239  halfnqq  7242  prarloclemarch2  7251  prarloclemlt  7325  prarloclemcalc  7334  genpelxp  7343  ltexprlempr  7440  recexprlempr  7464  cauappcvgprlemcl  7485  cauappcvgprlemladd  7490  caucvgprlemcl  7508  caucvgprprlemcl  7536  suplocexprlemell  7545  suplocexprlemdisj  7552  suplocexprlemub  7555  0r  7582  1sr  7583  m1r  7584  m1p1sr  7592  m1m1sr  7593  0lt1sr  7597  1ne0sr  7598  1idsr  7600  recexgt0sr  7605  prsradd  7618  caucvgsrlemoffres  7632  caucvgsr  7634  mappsrprg  7636  map2psrprg  7637  pitonnlem1p1  7678  pitonnlem2  7679  pitoregt0  7681  peano2nnnn  7685  axi2m1  7707  axprecex  7712  axcnre  7713  nnindnn  7725  nntopi  7726  0cn  7782  addcli  7794  mulcli  7795  mulcomi  7796  readdcli  7803  remulcli  7804  rexpssxrxp  7834  ltrelxr  7849  gtneii  7883  lttri3i  7885  letri3i  7886  ltnsymi  7887  lenlti  7888  ltlei  7889  mulgt0i  7897  mulgt0ii  7898  0lt1  7913  addcomi  7930  pncan3oi  8002  resubcli  8049  subcli  8062  pncan3i  8063  negsubi  8064  subnegi  8065  subeq0i  8066  neg11i  8067  negcon1i  8068  negcon2i  8069  mulneg1i  8190  mulneg2i  8191  mul2negi  8192  addgt0ii  8277  ltnegi  8279  lenegi  8280  ltnegcon2i  8281  lesub0i  8282  ltaddposi  8283  posdifi  8284  ltnegcon1i  8285  lenegcon1i  8286  subge0i  8287  1ap0  8376  ltapii  8421  recrecapi  8528  dividapi  8529  div0api  8530  rec11apii  8545  divdiv32api  8551  recgt0ii  8689  ltrecii  8700  ltdiv23ii  8709  sup3exmid  8739  nnssre  8748  nnind  8760  nnmulcli  8766  nnsubi  8784  0le2  8834  1lt3  8915  2lt4  8917  1lt4  8918  3lt5  8920  2lt5  8921  1lt5  8922  4lt6  8924  3lt6  8925  2lt6  8926  1lt6  8927  5lt7  8929  4lt7  8930  3lt7  8931  2lt7  8932  1lt7  8933  6lt8  8935  5lt8  8936  4lt8  8937  3lt8  8938  2lt8  8939  1lt8  8940  7lt9  8942  6lt9  8943  5lt9  8944  4lt9  8945  3lt9  8946  2lt9  8947  1lt9  8948  2muline0  8969  nn0addcli  9038  nn0mulcli  9039  nn0addge1i  9049  nn0addge2i  9050  dfz2  9147  halfnz  9171  9p1e10  9208  numnncl  9215  numltc  9231  le9lt10  9232  nummac  9250  8lt10  9337  7lt10  9338  6lt10  9339  5lt10  9340  4lt10  9341  3lt10  9342  2lt10  9343  1lt10  9344  eluzaddi  9376  eluzsubi  9377  eluz2nn  9388  eluz4eluz2  9389  uzuzle23  9393  eluzge3nn  9394  divfnzn  9440  elq  9441  qreccl  9461  xrltnr  9596  mnfltpnf  9601  xaddmnf1  9661  pnfaddmnf  9663  mnfaddpnf  9664  xrex  9669  xaddid1  9675  xsubge0  9694  xposdif  9695  xleaddadd  9700  elicc2i  9752  ioomax  9761  iccmax  9762  ioopos  9763  elxrge0  9791  iccshftri  9808  iccshftli  9810  iccdili  9812  icccntri  9814  unitssre  9818  fz10  9857  fzpreddisj  9882  fldiv4p1lem1div2  10109  frecfzennn  10230  fnn0nninf  10241  fxnn0nninf  10242  0tonninf  10243  1tonninf  10244  m1expcl2  10346  m1expcl  10347  nn0expcli  10350  sqmuli  10406  cu2  10422  i3  10425  subsqi  10433  binom2subi  10438  bcpasc  10544  4bc2eq6  10552  hashinfom  10556  prhash2ex  10587  hashp1i  10588  rei  10703  imi  10704  readdi  10732  imaddi  10733  remuli  10734  immuli  10735  cjaddi  10736  cjmuli  10737  ipcni  10738  crrei  10740  crimi  10741  rexfiuz  10793  sqrt1  10850  sqrt4  10851  sqrt9  10852  abs1  10876  sqrtmulii  10938  abslti  10942  abslei  10943  abssubi  10954  absmuli  10955  sqabsaddi  10956  sqabssubi  10957  abstrii  10959  fimaxre2  11030  climz  11093  abscn2  11116  recn2  11118  imcn2  11119  climabs  11121  climre  11123  climim  11124  fsumcnv  11238  fsumrelem  11272  fsumre  11273  fsumim  11274  arisum2  11300  expcnv  11305  geo2sum2  11316  geo2lim  11317  0.999...  11322  geoihalfsum  11323  ege2le3  11414  ef0  11415  reeff1  11443  tan0  11474  ef01bndlem  11499  sin01bnd  11500  cos01bnd  11501  cos1bnd  11502  cos2bnd  11503  sin01gt0  11504  cos01gt0  11505  sin02gt0  11506  sincos1sgn  11507  sincos2sgn  11508  cos12dec  11510  egt2lt3  11522  epos  11523  ene1  11527  eap1  11528  3dvdsdec  11598  3dvds2dec  11599  odd2np1lem  11605  n2dvds1  11645  z4even  11649  ndvdsi  11666  flodddiv4  11667  gcd0val  11685  6gcd4e2  11719  3lcm2e6woprm  11803  6lcm4e12  11804  3lcm2e6  11874  sqrt2irrlem  11875  phimullem  11937  xpnnen  11943  xpomen  11944  ennnfonelemj0  11950  ennnfonelem0  11954  ennnfonelemhf1o  11962  exmidunben  11975  qnnen  11980  unct  11991  setscom  12038  strleun  12087  txtopi  12469  txunii  12472  upxp  12480  uptx  12482  cnmpt1st  12496  cnmpt2nd  12497  txswaphmeolem  12528  qtopbasss  12729  cnmet  12738  cnopncntop  12745  remet  12748  blssioo  12753  tgqioo  12755  tgioo2cntop  12757  divcnap  12763  abscncf  12780  recncf  12781  imcncf  12782  cjcncf  12783  mulc1cncf  12784  cncfcn1cntop  12789  cdivcncfap  12795  expcncf  12800  cnrehmeocntop  12801  limccnp2lem  12853  limccnp2cntop  12854  dvcnp2cntop  12871  dvaddxxbr  12873  dvmulxxbr  12874  dvcoapbr  12879  dvrecap  12885  dveflem  12895  dvef  12896  sincn  12898  coscn  12899  reeff1oleme  12901  reeff1o  12902  cosz12  12909  sin0pilem1  12910  sin0pilem2  12911  pipos  12917  sinhalfpilem  12920  sincosq1lem  12954  sincosq1sgn  12955  sincosq2sgn  12956  sincosq3sgn  12957  sincosq4sgn  12958  sinq12gt0  12959  cosq14gt0  12961  cosq23lt0  12962  coseq0q4123  12963  coseq00topi  12964  coseq0negpitopi  12965  tangtx  12967  sincos4thpi  12969  tan4thpi  12970  sincos6thpi  12971  pigt3  12973  cosordlem  12978  cosq34lt1  12979  cos02pilt1  12980  cos0pilt1  12981  ioocosf1o  12983  negpitopissre  12984  log1  12995  loge  12996  2logb9irr  13096  sqrt2cxp2logb9e3  13100  2logb9irrap  13102  ex-fl  13108  ex-ceil  13109  ex-bc  13112  ex-dvds  13113  ex-gcd  13114  bj-unex  13288  bj-nn0suc0  13319  bj-nntrans  13320  bj-nnelirr  13322  pw1dom2  13361  012of  13363  2o01f  13364  pwle2  13366  nnsf  13374  peano3nninf  13376  nninfex  13380  exmidsbthrlem  13392  sbthom  13396  isomninnlem  13400  trilpolemisumle  13406  trilpolemeq1  13408  trilpolemlt1  13409  apdiff  13416  iswomninnlem  13417  ismkvnnlem  13419  dceqnconst  13423  iooref1o  13426  taupi  13430