Theorem mp2an 426

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 424	. 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  427  jaoi  716  mp3an  1337  barbara  2124  eqeq12i  2191  vtocl2  2794  spc2ev  2835  sbc2ie  3036  csbieb  3100  sseq12i  3185  uneq12i  3289  ineq12i  3336  ifssun  3550  nelpri  3618  ralpr  3649  rexpr  3650  preq12i  3676  dfop  3779  opeq12i  3785  breq12i  4014  mpteq2ia  4091  exmidundif  4208  exmidundifim  4209  opex  4231  opi2  4235  opth2  4242  opeqsn  4254  opeqpr  4255  uniop  4257  opelopaba  4268  braba  4269  opelopab  4273  brab  4274  opelopabaf  4275  unex  4443  snnex  4450  op1stb  4480  ifelpwun  4485  onun2i  4492  onsucssi  4507  ontriexmidim  4523  ontr2exmid  4526  onsucsssucexmid  4528  onsucelsucexmid  4531  opthreg  4557  tfis  4584  finds  4601  finds2  4602  nnregexmid  4622  xpeq12i  4650  opelvv  4678  eqrelriiv  4722  eqrelrdv  4724  xpss  4736  xpex  4743  relop  4779  brco  4800  opelcnv  4811  brcnv  4812  asymref  5016  codir  5019  ssrnres  5073  dmprop  5105  dfco2  5130  cossxp  5153  cocnvss  5156  coex  5176  funsn  5266  fnsn  5272  feq23i  5362  resasplitss  5397  fabex  5406  fvex  5537  xpsn  5695  fmptap  5709  opabex  5743  acexmidlemv  5876  oveq12i  5890  oprabid  5910  oprabss  5964  caovcom  6035  opabex3  6126  iunex  6127  oprabex  6132  ofmres  6140  op1st  6150  op2nd  6151  fo1st  6161  fo2nd  6162  mpoex  6218  1stconst  6225  2ndconst  6226  algrflem  6233  dftpos4  6267  tpostpos  6268  tpossym  6280  frecex  6398  frecfnom  6405  sucinc  6449  fnoei  6456  oeiexg  6457  nnacli  6486  nnmcli  6487  elec  6577  ecovcom  6645  ecovass  6647  ecovdi  6649  fnmap  6658  mapval  6663  elmap  6680  elpm  6682  elpm2  6683  map0  6692  ixpconst  6711  entri  6789  endisj  6827  xpcomco  6829  phplem2  6856  ssfiexmid  6879  domfiexmid  6881  unfiexmid  6920  unfiin  6928  inresflem  7062  casefun  7087  caserel  7089  caseinj  7091  omp1eomlem  7096  omp1eom  7097  endjusym  7098  djufun  7106  djuinj  7108  ctssdccl  7113  ctssdclemr  7114  nninfex  7123  infnninf  7125  fodjuomnilemdc  7145  ctssexmid  7151  exmidonfinlem  7195  dju1p1e2  7199  exmidfodomrlemr  7204  exmidfodomrlemrALT  7205  exmidaclem  7210  pw1dom2  7229  onntri35  7239  onntri45  7243  2oneel  7258  2omotaplemst  7260  1lt2pi  7342  indpi  7344  1nq  7368  rec1nq  7397  1lt2nq  7408  ltaddnq  7409  halfnqq  7412  prarloclemarch2  7421  prarloclemlt  7495  prarloclemcalc  7504  genpelxp  7513  ltexprlempr  7610  recexprlempr  7634  cauappcvgprlemcl  7655  cauappcvgprlemladd  7660  caucvgprlemcl  7678  caucvgprprlemcl  7706  suplocexprlemell  7715  suplocexprlemdisj  7722  suplocexprlemub  7725  0r  7752  1sr  7753  m1r  7754  m1p1sr  7762  m1m1sr  7763  0lt1sr  7767  1ne0sr  7768  1idsr  7770  recexgt0sr  7775  prsradd  7788  caucvgsrlemoffres  7802  caucvgsr  7804  mappsrprg  7806  map2psrprg  7807  pitonnlem1p1  7848  pitonnlem2  7849  pitoregt0  7851  peano2nnnn  7855  axi2m1  7877  axprecex  7882  axcnre  7883  nnindnn  7895  nntopi  7896  0cn  7952  addcli  7964  mulcli  7965  mulcomi  7966  readdcli  7973  remulcli  7974  rexpssxrxp  8005  ltrelxr  8021  gtneii  8056  lttri3i  8058  letri3i  8059  ltnsymi  8060  lenlti  8061  ltlei  8062  mulgt0i  8070  mulgt0ii  8071  0lt1  8087  addcomi  8104  pncan3oi  8176  resubcli  8223  subcli  8236  pncan3i  8237  negsubi  8238  subnegi  8239  subeq0i  8240  neg11i  8241  negcon1i  8242  negcon2i  8243  mulneg1i  8364  mulneg2i  8365  mul2negi  8366  addgt0ii  8451  ltnegi  8453  lenegi  8454  ltnegcon2i  8455  lesub0i  8456  ltaddposi  8457  posdifi  8458  ltnegcon1i  8459  lenegcon1i  8460  subge0i  8461  1ap0  8550  ltapii  8595  recrecapi  8704  dividapi  8705  div0api  8706  rec11apii  8721  divdiv32api  8727  recgt0ii  8867  ltrecii  8878  ltdiv23ii  8887  sup3exmid  8917  nnssre  8926  nnind  8938  nnmulcli  8944  nnsubi  8962  0le2  9012  1lt3  9093  2lt4  9095  1lt4  9096  3lt5  9098  2lt5  9099  1lt5  9100  4lt6  9102  3lt6  9103  2lt6  9104  1lt6  9105  5lt7  9107  4lt7  9108  3lt7  9109  2lt7  9110  1lt7  9111  6lt8  9113  5lt8  9114  4lt8  9115  3lt8  9116  2lt8  9117  1lt8  9118  7lt9  9120  6lt9  9121  5lt9  9122  4lt9  9123  3lt9  9124  2lt9  9125  1lt9  9126  2muline0  9147  nn0addcli  9216  nn0mulcli  9217  nn0addge1i  9227  nn0addge2i  9228  dfz2  9328  halfnz  9352  9p1e10  9389  numnncl  9396  numltc  9412  le9lt10  9413  nummac  9431  8lt10  9518  7lt10  9519  6lt10  9520  5lt10  9521  4lt10  9522  3lt10  9523  2lt10  9524  1lt10  9525  eluzaddi  9557  eluzsubi  9558  eluz2nn  9569  eluz4eluz2  9570  uzuzle23  9574  eluzge3nn  9575  divfnzn  9624  elq  9625  qreccl  9645  xrltnr  9782  mnfltpnf  9788  xaddmnf1  9851  pnfaddmnf  9853  mnfaddpnf  9854  xrex  9859  xaddid1  9865  xsubge0  9884  xposdif  9885  xleaddadd  9890  elicc2i  9942  ioomax  9951  iccmax  9952  ioopos  9953  elxrge0  9981  iccshftri  9998  iccshftli  10000  iccdili  10002  icccntri  10004  unitssre  10008  fz10  10049  fzpreddisj  10074  fz0to4untppr  10127  dfrp2  10267  fldiv4p1lem1div2  10308  frecfzennn  10429  fnn0nninf  10440  fxnn0nninf  10441  0tonninf  10442  1tonninf  10443  m1expcl2  10545  m1expcl  10546  nn0expcli  10549  sqmuli  10606  cu2  10622  i3  10625  subsqi  10633  binom2subi  10639  bcpasc  10749  4bc2eq6  10757  hashinfom  10761  prhash2ex  10792  hashp1i  10793  rei  10911  imi  10912  readdi  10940  imaddi  10941  remuli  10942  immuli  10943  cjaddi  10944  cjmuli  10945  ipcni  10946  crrei  10948  crimi  10949  rexfiuz  11001  sqrt1  11058  sqrt4  11059  sqrt9  11060  abs1  11084  sqrtmulii  11146  abslti  11150  abslei  11151  abssubi  11162  absmuli  11163  sqabsaddi  11164  sqabssubi  11165  abstrii  11167  fimaxre2  11238  climz  11303  abscn2  11326  recn2  11328  imcn2  11329  climabs  11331  climre  11333  climim  11334  fsumcnv  11448  fsumrelem  11482  fsumre  11483  fsumim  11484  arisum2  11510  expcnv  11515  geo2sum2  11526  geo2lim  11527  0.999...  11532  geoihalfsum  11533  fprodcnv  11636  fprodge0  11648  fprodge1  11650  ege2le3  11682  ef0  11683  reeff1  11711  tan0  11742  ef01bndlem  11767  sin01bnd  11768  cos01bnd  11769  cos1bnd  11770  cos2bnd  11771  sin01gt0  11772  cos01gt0  11773  sin02gt0  11774  sincos1sgn  11775  sincos2sgn  11776  cos12dec  11778  egt2lt3  11790  epos  11791  ene1  11795  eap1  11796  3dvdsdec  11873  3dvds2dec  11874  odd2np1lem  11880  n2dvds1  11920  z4even  11924  ndvdsi  11941  flodddiv4  11942  gcd0val  11964  6gcd4e2  11999  3lcm2e6woprm  12089  6lcm4e12  12090  3lcm2e6  12163  sqrt2irrlem  12164  phimullem  12228  pockthi  12359  xpnnen  12398  xpomen  12399  ennnfonelemj0  12405  ennnfonelem0  12409  ennnfonelemhf1o  12417  exmidunben  12430  qnnen  12435  unct  12446  setscom  12505  strleun  12566  prdsex  12724  imasival  12733  ismgm  12782  fn0g  12800  issgrp  12815  ismnddef  12825  isring  13189  mgpf  13200  rmodislmod  13447  lidlmex  13564  cnfldstr  13597  cnfldcj  13602  cnfld0  13605  cnfldplusf  13608  zringcrng  13622  zringmulr  13629  zringmpg  13636  txtopi  13901  txunii  13904  upxp  13912  uptx  13914  cnmpt1st  13928  cnmpt2nd  13929  txswaphmeolem  13960  qtopbasss  14161  cnmet  14170  cnopncntop  14177  remet  14180  blssioo  14185  tgqioo  14187  tgioo2cntop  14189  divcnap  14195  abscncf  14212  recncf  14213  imcncf  14214  cjcncf  14215  mulc1cncf  14216  cncfcn1cntop  14221  cdivcncfap  14227  expcncf  14232  cnrehmeocntop  14233  limccnp2lem  14285  limccnp2cntop  14286  dvcnp2cntop  14303  dvaddxxbr  14305  dvmulxxbr  14306  dvcoapbr  14311  dvrecap  14317  dveflem  14327  dvef  14328  sincn  14330  coscn  14331  reeff1oleme  14333  reeff1o  14334  cosz12  14341  sin0pilem1  14342  sin0pilem2  14343  pipos  14349  sinhalfpilem  14352  sincosq1lem  14386  sincosq1sgn  14387  sincosq2sgn  14388  sincosq3sgn  14389  sincosq4sgn  14390  sinq12gt0  14391  cosq14gt0  14393  cosq23lt0  14394  coseq0q4123  14395  coseq00topi  14396  coseq0negpitopi  14397  tangtx  14399  sincos4thpi  14401  tan4thpi  14402  sincos6thpi  14403  pigt3  14405  cosordlem  14410  cosq34lt1  14411  cos02pilt1  14412  cos0pilt1  14413  ioocosf1o  14415  negpitopissre  14416  log1  14427  loge  14428  2logb9irr  14529  sqrt2cxp2logb9e3  14533  2logb9irrap  14535  lgsdir2lem2  14570  lgsdir2lem3  14571  2lgsoddprmlem3  14599  2sqlem9  14611  2sqlem10  14612  ex-fl  14617  ex-ceil  14618  ex-bc  14621  ex-dvds  14622  ex-gcd  14623  bj-charfunbi  14703  bj-unex  14811  bj-nn0suc0  14842  bj-nntrans  14843  bj-nnelirr  14845  012of  14886  2o01f  14887  pwle2  14889  nnsf  14895  peano3nninf  14897  exmidsbthrlem  14911  sbthom  14915  isomninnlem  14919  iooref1o  14923  trilpolemisumle  14927  trilpolemeq1  14929  trilpolemlt1  14930  apdiff  14937  iswomninnlem  14938  iswomni0  14940  ismkvnnlem  14941  dceqnconst  14949  dcapnconst  14950  nconstwlpolemgt0  14953  taupi  14962