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  1327  barbara  2112  eqeq12i  2179  vtocl2  2780  spc2ev  2821  sbc2ie  3021  csbieb  3085  sseq12i  3169  uneq12i  3273  ineq12i  3320  ifssun  3533  nelpri  3599  ralpr  3630  rexpr  3631  preq12i  3657  dfop  3756  opeq12i  3762  breq12i  3990  mpteq2ia  4067  exmidundif  4184  exmidundifim  4185  opex  4206  opi2  4210  opth2  4217  opeqsn  4229  opeqpr  4230  uniop  4232  opelopaba  4243  braba  4244  opelopab  4248  brab  4249  opelopabaf  4250  unex  4418  snnex  4425  op1stb  4455  ifelpwun  4460  onun2i  4467  onsucssi  4482  ontriexmidim  4498  ontr2exmid  4501  onsucsssucexmid  4503  onsucelsucexmid  4506  opthreg  4532  tfis  4559  finds  4576  finds2  4577  nnregexmid  4597  xpeq12i  4625  opelvv  4653  eqrelriiv  4697  eqrelrdv  4699  xpss  4711  xpex  4718  relop  4753  brco  4774  opelcnv  4785  brcnv  4786  asymref  4988  codir  4991  ssrnres  5045  dmprop  5077  dfco2  5102  cossxp  5125  cocnvss  5128  coex  5148  funsn  5235  fnsn  5241  feq23i  5331  resasplitss  5366  fabex  5375  fvex  5505  xpsn  5660  fmptap  5674  opabex  5708  acexmidlemv  5839  oveq12i  5853  oprabid  5870  oprabss  5924  caovcom  5995  opabex3  6087  iunex  6088  oprabex  6093  ofmres  6101  op1st  6111  op2nd  6112  fo1st  6122  fo2nd  6123  mpoex  6178  1stconst  6185  2ndconst  6186  algrflem  6193  dftpos4  6227  tpostpos  6228  tpossym  6240  frecex  6358  frecfnom  6365  sucinc  6409  fnoei  6416  oeiexg  6417  nnacli  6446  nnmcli  6447  elec  6536  ecovcom  6604  ecovass  6606  ecovdi  6608  fnmap  6617  mapval  6622  elmap  6639  elpm  6641  elpm2  6642  map0  6651  ixpconst  6670  entri  6748  endisj  6786  xpcomco  6788  phplem2  6815  ssfiexmid  6838  domfiexmid  6840  unfiexmid  6879  unfiin  6887  inresflem  7021  casefun  7046  caserel  7048  caseinj  7050  omp1eomlem  7055  omp1eom  7056  endjusym  7057  djufun  7065  djuinj  7067  ctssdccl  7072  ctssdclemr  7073  nninfex  7082  infnninf  7084  fodjuomnilemdc  7104  ctssexmid  7110  exmidonfinlem  7145  dju1p1e2  7149  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  exmidaclem  7160  pw1dom2  7179  onntri35  7189  onntri45  7193  1lt2pi  7277  indpi  7279  1nq  7303  rec1nq  7332  1lt2nq  7343  ltaddnq  7344  halfnqq  7347  prarloclemarch2  7356  prarloclemlt  7430  prarloclemcalc  7439  genpelxp  7448  ltexprlempr  7545  recexprlempr  7569  cauappcvgprlemcl  7590  cauappcvgprlemladd  7595  caucvgprlemcl  7613  caucvgprprlemcl  7641  suplocexprlemell  7650  suplocexprlemdisj  7657  suplocexprlemub  7660  0r  7687  1sr  7688  m1r  7689  m1p1sr  7697  m1m1sr  7698  0lt1sr  7702  1ne0sr  7703  1idsr  7705  recexgt0sr  7710  prsradd  7723  caucvgsrlemoffres  7737  caucvgsr  7739  mappsrprg  7741  map2psrprg  7742  pitonnlem1p1  7783  pitonnlem2  7784  pitoregt0  7786  peano2nnnn  7790  axi2m1  7812  axprecex  7817  axcnre  7818  nnindnn  7830  nntopi  7831  0cn  7887  addcli  7899  mulcli  7900  mulcomi  7901  readdcli  7908  remulcli  7909  rexpssxrxp  7939  ltrelxr  7955  gtneii  7990  lttri3i  7992  letri3i  7993  ltnsymi  7994  lenlti  7995  ltlei  7996  mulgt0i  8004  mulgt0ii  8005  0lt1  8021  addcomi  8038  pncan3oi  8110  resubcli  8157  subcli  8170  pncan3i  8171  negsubi  8172  subnegi  8173  subeq0i  8174  neg11i  8175  negcon1i  8176  negcon2i  8177  mulneg1i  8298  mulneg2i  8299  mul2negi  8300  addgt0ii  8385  ltnegi  8387  lenegi  8388  ltnegcon2i  8389  lesub0i  8390  ltaddposi  8391  posdifi  8392  ltnegcon1i  8393  lenegcon1i  8394  subge0i  8395  1ap0  8484  ltapii  8529  recrecapi  8636  dividapi  8637  div0api  8638  rec11apii  8653  divdiv32api  8659  recgt0ii  8798  ltrecii  8809  ltdiv23ii  8818  sup3exmid  8848  nnssre  8857  nnind  8869  nnmulcli  8875  nnsubi  8893  0le2  8943  1lt3  9024  2lt4  9026  1lt4  9027  3lt5  9029  2lt5  9030  1lt5  9031  4lt6  9033  3lt6  9034  2lt6  9035  1lt6  9036  5lt7  9038  4lt7  9039  3lt7  9040  2lt7  9041  1lt7  9042  6lt8  9044  5lt8  9045  4lt8  9046  3lt8  9047  2lt8  9048  1lt8  9049  7lt9  9051  6lt9  9052  5lt9  9053  4lt9  9054  3lt9  9055  2lt9  9056  1lt9  9057  2muline0  9078  nn0addcli  9147  nn0mulcli  9148  nn0addge1i  9158  nn0addge2i  9159  dfz2  9259  halfnz  9283  9p1e10  9320  numnncl  9327  numltc  9343  le9lt10  9344  nummac  9362  8lt10  9449  7lt10  9450  6lt10  9451  5lt10  9452  4lt10  9453  3lt10  9454  2lt10  9455  1lt10  9456  eluzaddi  9488  eluzsubi  9489  eluz2nn  9500  eluz4eluz2  9501  uzuzle23  9505  eluzge3nn  9506  divfnzn  9555  elq  9556  qreccl  9576  xrltnr  9711  mnfltpnf  9717  xaddmnf1  9780  pnfaddmnf  9782  mnfaddpnf  9783  xrex  9788  xaddid1  9794  xsubge0  9813  xposdif  9814  xleaddadd  9819  elicc2i  9871  ioomax  9880  iccmax  9881  ioopos  9882  elxrge0  9910  iccshftri  9927  iccshftli  9929  iccdili  9931  icccntri  9933  unitssre  9937  fz10  9977  fzpreddisj  10002  fz0to4untppr  10055  dfrp2  10195  fldiv4p1lem1div2  10236  frecfzennn  10357  fnn0nninf  10368  fxnn0nninf  10369  0tonninf  10370  1tonninf  10371  m1expcl2  10473  m1expcl  10474  nn0expcli  10477  sqmuli  10533  cu2  10549  i3  10552  subsqi  10560  binom2subi  10566  bcpasc  10675  4bc2eq6  10683  hashinfom  10687  prhash2ex  10718  hashp1i  10719  rei  10837  imi  10838  readdi  10866  imaddi  10867  remuli  10868  immuli  10869  cjaddi  10870  cjmuli  10871  ipcni  10872  crrei  10874  crimi  10875  rexfiuz  10927  sqrt1  10984  sqrt4  10985  sqrt9  10986  abs1  11010  sqrtmulii  11072  abslti  11076  abslei  11077  abssubi  11088  absmuli  11089  sqabsaddi  11090  sqabssubi  11091  abstrii  11093  fimaxre2  11164  climz  11229  abscn2  11252  recn2  11254  imcn2  11255  climabs  11257  climre  11259  climim  11260  fsumcnv  11374  fsumrelem  11408  fsumre  11409  fsumim  11410  arisum2  11436  expcnv  11441  geo2sum2  11452  geo2lim  11453  0.999...  11458  geoihalfsum  11459  fprodcnv  11562  fprodge0  11574  fprodge1  11576  ege2le3  11608  ef0  11609  reeff1  11637  tan0  11668  ef01bndlem  11693  sin01bnd  11694  cos01bnd  11695  cos1bnd  11696  cos2bnd  11697  sin01gt0  11698  cos01gt0  11699  sin02gt0  11700  sincos1sgn  11701  sincos2sgn  11702  cos12dec  11704  egt2lt3  11716  epos  11717  ene1  11721  eap1  11722  3dvdsdec  11798  3dvds2dec  11799  odd2np1lem  11805  n2dvds1  11845  z4even  11849  ndvdsi  11866  flodddiv4  11867  gcd0val  11889  6gcd4e2  11924  3lcm2e6woprm  12014  6lcm4e12  12015  3lcm2e6  12088  sqrt2irrlem  12089  phimullem  12153  pockthi  12284  xpnnen  12323  xpomen  12324  ennnfonelemj0  12330  ennnfonelem0  12334  ennnfonelemhf1o  12342  exmidunben  12355  qnnen  12360  unct  12371  setscom  12430  strleun  12479  txtopi  12861  txunii  12864  upxp  12872  uptx  12874  cnmpt1st  12888  cnmpt2nd  12889  txswaphmeolem  12920  qtopbasss  13121  cnmet  13130  cnopncntop  13137  remet  13140  blssioo  13145  tgqioo  13147  tgioo2cntop  13149  divcnap  13155  abscncf  13172  recncf  13173  imcncf  13174  cjcncf  13175  mulc1cncf  13176  cncfcn1cntop  13181  cdivcncfap  13187  expcncf  13192  cnrehmeocntop  13193  limccnp2lem  13245  limccnp2cntop  13246  dvcnp2cntop  13263  dvaddxxbr  13265  dvmulxxbr  13266  dvcoapbr  13271  dvrecap  13277  dveflem  13287  dvef  13288  sincn  13290  coscn  13291  reeff1oleme  13293  reeff1o  13294  cosz12  13301  sin0pilem1  13302  sin0pilem2  13303  pipos  13309  sinhalfpilem  13312  sincosq1lem  13346  sincosq1sgn  13347  sincosq2sgn  13348  sincosq3sgn  13349  sincosq4sgn  13350  sinq12gt0  13351  cosq14gt0  13353  cosq23lt0  13354  coseq0q4123  13355  coseq00topi  13356  coseq0negpitopi  13357  tangtx  13359  sincos4thpi  13361  tan4thpi  13362  sincos6thpi  13363  pigt3  13365  cosordlem  13370  cosq34lt1  13371  cos02pilt1  13372  cos0pilt1  13373  ioocosf1o  13375  negpitopissre  13376  log1  13387  loge  13388  2logb9irr  13489  sqrt2cxp2logb9e3  13493  2logb9irrap  13495  lgsdir2lem2  13530  lgsdir2lem3  13531  2sqlem9  13560  2sqlem10  13561  ex-fl  13566  ex-ceil  13567  ex-bc  13570  ex-dvds  13571  ex-gcd  13572  bj-charfunbi  13653  bj-unex  13761  bj-nn0suc0  13792  bj-nntrans  13793  bj-nnelirr  13795  012of  13835  2o01f  13836  pwle2  13838  nnsf  13845  peano3nninf  13847  exmidsbthrlem  13861  sbthom  13865  isomninnlem  13869  iooref1o  13873  trilpolemisumle  13877  trilpolemeq1  13879  trilpolemlt1  13880  apdiff  13887  iswomninnlem  13888  iswomni0  13890  ismkvnnlem  13891  dceqnconst  13898  dcapnconst  13899  nconstwlpolemgt0  13902  taupi  13909