Theorem mp2an 422

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 420	. 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  423  jaoi  705  mp3an  1315  barbara  2097  eqeq12i  2153  vtocl2  2741  spc2ev  2781  sbc2ie  2980  csbieb  3041  sseq12i  3125  uneq12i  3228  ineq12i  3275  nelpri  3551  ralpr  3578  rexpr  3579  preq12i  3605  dfop  3704  opeq12i  3710  breq12i  3938  mpteq2ia  4014  exmidundif  4129  exmidundifim  4130  opex  4151  opi2  4155  opth2  4162  opeqsn  4174  opeqpr  4175  uniop  4177  opelopaba  4188  braba  4189  opelopab  4193  brab  4194  opelopabaf  4195  unex  4362  snnex  4369  op1stb  4399  onun2i  4407  onsucssi  4422  ontr2exmid  4440  onsucsssucexmid  4442  onsucelsucexmid  4445  opthreg  4471  tfis  4497  finds  4514  finds2  4515  nnregexmid  4534  xpeq12i  4561  opelvv  4589  eqrelriiv  4633  eqrelrdv  4635  xpss  4647  xpex  4654  relop  4689  brco  4710  opelcnv  4721  brcnv  4722  asymref  4924  codir  4927  ssrnres  4981  dmprop  5013  dfco2  5038  cossxp  5061  cocnvss  5064  coex  5084  funsn  5171  fnsn  5177  feq23i  5267  resasplitss  5302  fabex  5311  fvex  5441  xpsn  5596  fmptap  5610  opabex  5644  acexmidlemv  5772  oveq12i  5786  oprabid  5803  oprabss  5857  caovcom  5928  opabex3  6020  iunex  6021  oprabex  6026  ofmres  6034  op1st  6044  op2nd  6045  fo1st  6055  fo2nd  6056  mpoex  6111  1stconst  6118  2ndconst  6119  algrflem  6126  dftpos4  6160  tpostpos  6161  tpossym  6173  frecex  6291  frecfnom  6298  sucinc  6341  fnoei  6348  oeiexg  6349  nnacli  6378  nnmcli  6379  elec  6468  ecovcom  6536  ecovass  6538  ecovdi  6540  fnmap  6549  mapval  6554  elmap  6571  elpm  6573  elpm2  6574  map0  6583  ixpconst  6602  entri  6680  endisj  6718  xpcomco  6720  phplem2  6747  ssfiexmid  6770  domfiexmid  6772  unfiexmid  6806  unfiin  6814  inresflem  6945  casefun  6970  caserel  6972  caseinj  6974  omp1eomlem  6979  omp1eom  6980  endjusym  6981  djufun  6989  djuinj  6991  ctssdccl  6996  ctssdclemr  6997  fodjuomnilemdc  7016  ctssexmid  7024  exmidonfinlem  7049  dju1p1e2  7053  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  exmidaclem  7064  1lt2pi  7148  indpi  7150  1nq  7174  rec1nq  7203  1lt2nq  7214  ltaddnq  7215  halfnqq  7218  prarloclemarch2  7227  prarloclemlt  7301  prarloclemcalc  7310  genpelxp  7319  ltexprlempr  7416  recexprlempr  7440  cauappcvgprlemcl  7461  cauappcvgprlemladd  7466  caucvgprlemcl  7484  caucvgprprlemcl  7512  suplocexprlemell  7521  suplocexprlemdisj  7528  suplocexprlemub  7531  0r  7558  1sr  7559  m1r  7560  m1p1sr  7568  m1m1sr  7569  0lt1sr  7573  1ne0sr  7574  1idsr  7576  recexgt0sr  7581  prsradd  7594  caucvgsrlemoffres  7608  caucvgsr  7610  mappsrprg  7612  map2psrprg  7613  pitonnlem1p1  7654  pitonnlem2  7655  pitoregt0  7657  peano2nnnn  7661  axi2m1  7683  axprecex  7688  axcnre  7689  nnindnn  7701  nntopi  7702  0cn  7758  addcli  7770  mulcli  7771  mulcomi  7772  readdcli  7779  remulcli  7780  rexpssxrxp  7810  ltrelxr  7825  gtneii  7859  lttri3i  7861  letri3i  7862  ltnsymi  7863  lenlti  7864  ltlei  7865  mulgt0i  7873  mulgt0ii  7874  0lt1  7889  addcomi  7906  pncan3oi  7978  resubcli  8025  subcli  8038  pncan3i  8039  negsubi  8040  subnegi  8041  subeq0i  8042  neg11i  8043  negcon1i  8044  negcon2i  8045  mulneg1i  8166  mulneg2i  8167  mul2negi  8168  addgt0ii  8253  ltnegi  8255  lenegi  8256  ltnegcon2i  8257  lesub0i  8258  ltaddposi  8259  posdifi  8260  ltnegcon1i  8261  lenegcon1i  8262  subge0i  8263  1ap0  8352  ltapii  8397  recrecapi  8504  dividapi  8505  div0api  8506  rec11apii  8521  divdiv32api  8527  recgt0ii  8665  ltrecii  8676  ltdiv23ii  8685  sup3exmid  8715  nnssre  8724  nnind  8736  nnmulcli  8742  nnsubi  8760  0le2  8810  1lt3  8891  2lt4  8893  1lt4  8894  3lt5  8896  2lt5  8897  1lt5  8898  4lt6  8900  3lt6  8901  2lt6  8902  1lt6  8903  5lt7  8905  4lt7  8906  3lt7  8907  2lt7  8908  1lt7  8909  6lt8  8911  5lt8  8912  4lt8  8913  3lt8  8914  2lt8  8915  1lt8  8916  7lt9  8918  6lt9  8919  5lt9  8920  4lt9  8921  3lt9  8922  2lt9  8923  1lt9  8924  2muline0  8945  nn0addcli  9014  nn0mulcli  9015  nn0addge1i  9025  nn0addge2i  9026  dfz2  9123  halfnz  9147  9p1e10  9184  numnncl  9191  numltc  9207  le9lt10  9208  nummac  9226  8lt10  9313  7lt10  9314  6lt10  9315  5lt10  9316  4lt10  9317  3lt10  9318  2lt10  9319  1lt10  9320  eluzaddi  9352  eluzsubi  9353  eluz2nn  9364  uzuzle23  9366  eluzge3nn  9367  divfnzn  9413  elq  9414  qreccl  9434  xrltnr  9566  mnfltpnf  9571  xaddmnf1  9631  pnfaddmnf  9633  mnfaddpnf  9634  xrex  9639  xaddid1  9645  xsubge0  9664  xposdif  9665  xleaddadd  9670  elicc2i  9722  ioomax  9731  iccmax  9732  ioopos  9733  elxrge0  9761  iccshftri  9778  iccshftli  9780  iccdili  9782  icccntri  9784  unitssre  9788  fz10  9826  fzpreddisj  9851  fldiv4p1lem1div2  10078  frecfzennn  10199  fnn0nninf  10210  fxnn0nninf  10211  0tonninf  10212  1tonninf  10213  m1expcl2  10315  m1expcl  10316  nn0expcli  10319  sqmuli  10375  cu2  10391  i3  10394  subsqi  10402  binom2subi  10407  bcpasc  10512  4bc2eq6  10520  hashinfom  10524  prhash2ex  10555  hashp1i  10556  rei  10671  imi  10672  readdi  10700  imaddi  10701  remuli  10702  immuli  10703  cjaddi  10704  cjmuli  10705  ipcni  10706  crrei  10708  crimi  10709  rexfiuz  10761  sqrt1  10818  sqrt4  10819  sqrt9  10820  abs1  10844  sqrtmulii  10906  abslti  10910  abslei  10911  abssubi  10922  absmuli  10923  sqabsaddi  10924  sqabssubi  10925  abstrii  10927  fimaxre2  10998  climz  11061  abscn2  11084  recn2  11086  imcn2  11087  climabs  11089  climre  11091  climim  11092  fsumcnv  11206  fsumrelem  11240  fsumre  11241  fsumim  11242  arisum2  11268  expcnv  11273  geo2sum2  11284  geo2lim  11285  0.999...  11290  geoihalfsum  11291  ege2le3  11377  ef0  11378  reeff1  11407  tan0  11438  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  cos1bnd  11466  cos2bnd  11467  sin01gt0  11468  cos01gt0  11469  sin02gt0  11470  sincos1sgn  11471  sincos2sgn  11472  cos12dec  11474  egt2lt3  11486  epos  11487  ene1  11491  eap1  11492  3dvdsdec  11562  3dvds2dec  11563  odd2np1lem  11569  n2dvds1  11609  z4even  11613  ndvdsi  11630  flodddiv4  11631  gcd0val  11649  6gcd4e2  11683  3lcm2e6woprm  11767  6lcm4e12  11768  3lcm2e6  11838  sqrt2irrlem  11839  phimullem  11901  xpnnen  11907  xpomen  11908  ennnfonelemj0  11914  ennnfonelem0  11918  ennnfonelemhf1o  11926  exmidunben  11939  qnnen  11944  unct  11954  setscom  11999  strleun  12048  txtopi  12430  txunii  12433  upxp  12441  uptx  12443  cnmpt1st  12457  cnmpt2nd  12458  txswaphmeolem  12489  qtopbasss  12690  cnmet  12699  cnopncntop  12706  remet  12709  blssioo  12714  tgqioo  12716  tgioo2cntop  12718  divcnap  12724  abscncf  12741  recncf  12742  imcncf  12743  cjcncf  12744  mulc1cncf  12745  cncfcn1cntop  12750  cdivcncfap  12756  expcncf  12761  cnrehmeocntop  12762  limccnp2lem  12814  limccnp2cntop  12815  dvcnp2cntop  12832  dvaddxxbr  12834  dvmulxxbr  12835  dvcoapbr  12840  dvrecap  12846  dveflem  12855  dvef  12856  sincn  12858  coscn  12859  cosz12  12861  sin0pilem1  12862  sin0pilem2  12863  pipos  12869  sinhalfpilem  12872  sincosq1lem  12906  sincosq1sgn  12907  sincosq2sgn  12908  sincosq3sgn  12909  sincosq4sgn  12910  sinq12gt0  12911  cosq14gt0  12913  cosq23lt0  12914  coseq0q4123  12915  coseq00topi  12916  coseq0negpitopi  12917  tangtx  12919  sincos4thpi  12921  tan4thpi  12922  sincos6thpi  12923  pigt3  12925  cosordlem  12930  cosq34lt1  12931  cos02pilt1  12932  ex-fl  12937  ex-ceil  12938  ex-bc  12941  ex-dvds  12942  ex-gcd  12943  bj-unex  13117  bj-nn0suc0  13148  bj-nntrans  13149  bj-nnelirr  13151  pw1dom2  13190  pwle2  13193  nnsf  13199  peano3nninf  13201  nninfex  13205  exmidsbthrlem  13217  sbthom  13221  isomninnlem  13225  trilpolemisumle  13231  trilpolemeq1  13233  trilpolemlt1  13234  taupi  13239