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  2792  spc2ev  2833  sbc2ie  3034  csbieb  3098  sseq12i  3183  uneq12i  3287  ineq12i  3334  ifssun  3548  nelpri  3615  ralpr  3646  rexpr  3647  preq12i  3673  dfop  3775  opeq12i  3781  breq12i  4009  mpteq2ia  4086  exmidundif  4203  exmidundifim  4204  opex  4226  opi2  4230  opth2  4237  opeqsn  4249  opeqpr  4250  uniop  4252  opelopaba  4263  braba  4264  opelopab  4268  brab  4269  opelopabaf  4270  unex  4438  snnex  4445  op1stb  4475  ifelpwun  4480  onun2i  4487  onsucssi  4502  ontriexmidim  4518  ontr2exmid  4521  onsucsssucexmid  4523  onsucelsucexmid  4526  opthreg  4552  tfis  4579  finds  4596  finds2  4597  nnregexmid  4617  xpeq12i  4645  opelvv  4673  eqrelriiv  4717  eqrelrdv  4719  xpss  4731  xpex  4738  relop  4773  brco  4794  opelcnv  4805  brcnv  4806  asymref  5010  codir  5013  ssrnres  5067  dmprop  5099  dfco2  5124  cossxp  5147  cocnvss  5150  coex  5170  funsn  5260  fnsn  5266  feq23i  5356  resasplitss  5391  fabex  5400  fvex  5531  xpsn  5688  fmptap  5702  opabex  5736  acexmidlemv  5867  oveq12i  5881  oprabid  5901  oprabss  5955  caovcom  6026  opabex3  6117  iunex  6118  oprabex  6123  ofmres  6131  op1st  6141  op2nd  6142  fo1st  6152  fo2nd  6153  mpoex  6209  1stconst  6216  2ndconst  6217  algrflem  6224  dftpos4  6258  tpostpos  6259  tpossym  6271  frecex  6389  frecfnom  6396  sucinc  6440  fnoei  6447  oeiexg  6448  nnacli  6477  nnmcli  6478  elec  6568  ecovcom  6636  ecovass  6638  ecovdi  6640  fnmap  6649  mapval  6654  elmap  6671  elpm  6673  elpm2  6674  map0  6683  ixpconst  6702  entri  6780  endisj  6818  xpcomco  6820  phplem2  6847  ssfiexmid  6870  domfiexmid  6872  unfiexmid  6911  unfiin  6919  inresflem  7053  casefun  7078  caserel  7080  caseinj  7082  omp1eomlem  7087  omp1eom  7088  endjusym  7089  djufun  7097  djuinj  7099  ctssdccl  7104  ctssdclemr  7105  nninfex  7114  infnninf  7116  fodjuomnilemdc  7136  ctssexmid  7142  exmidonfinlem  7186  dju1p1e2  7190  exmidfodomrlemr  7195  exmidfodomrlemrALT  7196  exmidaclem  7201  pw1dom2  7220  onntri35  7230  onntri45  7234  2oneel  7246  2omotaplemst  7248  1lt2pi  7330  indpi  7332  1nq  7356  rec1nq  7385  1lt2nq  7396  ltaddnq  7397  halfnqq  7400  prarloclemarch2  7409  prarloclemlt  7483  prarloclemcalc  7492  genpelxp  7501  ltexprlempr  7598  recexprlempr  7622  cauappcvgprlemcl  7643  cauappcvgprlemladd  7648  caucvgprlemcl  7666  caucvgprprlemcl  7694  suplocexprlemell  7703  suplocexprlemdisj  7710  suplocexprlemub  7713  0r  7740  1sr  7741  m1r  7742  m1p1sr  7750  m1m1sr  7751  0lt1sr  7755  1ne0sr  7756  1idsr  7758  recexgt0sr  7763  prsradd  7776  caucvgsrlemoffres  7790  caucvgsr  7792  mappsrprg  7794  map2psrprg  7795  pitonnlem1p1  7836  pitonnlem2  7837  pitoregt0  7839  peano2nnnn  7843  axi2m1  7865  axprecex  7870  axcnre  7871  nnindnn  7883  nntopi  7884  0cn  7940  addcli  7952  mulcli  7953  mulcomi  7954  readdcli  7961  remulcli  7962  rexpssxrxp  7992  ltrelxr  8008  gtneii  8043  lttri3i  8045  letri3i  8046  ltnsymi  8047  lenlti  8048  ltlei  8049  mulgt0i  8057  mulgt0ii  8058  0lt1  8074  addcomi  8091  pncan3oi  8163  resubcli  8210  subcli  8223  pncan3i  8224  negsubi  8225  subnegi  8226  subeq0i  8227  neg11i  8228  negcon1i  8229  negcon2i  8230  mulneg1i  8351  mulneg2i  8352  mul2negi  8353  addgt0ii  8438  ltnegi  8440  lenegi  8441  ltnegcon2i  8442  lesub0i  8443  ltaddposi  8444  posdifi  8445  ltnegcon1i  8446  lenegcon1i  8447  subge0i  8448  1ap0  8537  ltapii  8582  recrecapi  8690  dividapi  8691  div0api  8692  rec11apii  8707  divdiv32api  8713  recgt0ii  8853  ltrecii  8864  ltdiv23ii  8873  sup3exmid  8903  nnssre  8912  nnind  8924  nnmulcli  8930  nnsubi  8948  0le2  8998  1lt3  9079  2lt4  9081  1lt4  9082  3lt5  9084  2lt5  9085  1lt5  9086  4lt6  9088  3lt6  9089  2lt6  9090  1lt6  9091  5lt7  9093  4lt7  9094  3lt7  9095  2lt7  9096  1lt7  9097  6lt8  9099  5lt8  9100  4lt8  9101  3lt8  9102  2lt8  9103  1lt8  9104  7lt9  9106  6lt9  9107  5lt9  9108  4lt9  9109  3lt9  9110  2lt9  9111  1lt9  9112  2muline0  9133  nn0addcli  9202  nn0mulcli  9203  nn0addge1i  9213  nn0addge2i  9214  dfz2  9314  halfnz  9338  9p1e10  9375  numnncl  9382  numltc  9398  le9lt10  9399  nummac  9417  8lt10  9504  7lt10  9505  6lt10  9506  5lt10  9507  4lt10  9508  3lt10  9509  2lt10  9510  1lt10  9511  eluzaddi  9543  eluzsubi  9544  eluz2nn  9555  eluz4eluz2  9556  uzuzle23  9560  eluzge3nn  9561  divfnzn  9610  elq  9611  qreccl  9631  xrltnr  9766  mnfltpnf  9772  xaddmnf1  9835  pnfaddmnf  9837  mnfaddpnf  9838  xrex  9843  xaddid1  9849  xsubge0  9868  xposdif  9869  xleaddadd  9874  elicc2i  9926  ioomax  9935  iccmax  9936  ioopos  9937  elxrge0  9965  iccshftri  9982  iccshftli  9984  iccdili  9986  icccntri  9988  unitssre  9992  fz10  10032  fzpreddisj  10057  fz0to4untppr  10110  dfrp2  10250  fldiv4p1lem1div2  10291  frecfzennn  10412  fnn0nninf  10423  fxnn0nninf  10424  0tonninf  10425  1tonninf  10426  m1expcl2  10528  m1expcl  10529  nn0expcli  10532  sqmuli  10588  cu2  10604  i3  10607  subsqi  10615  binom2subi  10621  bcpasc  10730  4bc2eq6  10738  hashinfom  10742  prhash2ex  10773  hashp1i  10774  rei  10892  imi  10893  readdi  10921  imaddi  10922  remuli  10923  immuli  10924  cjaddi  10925  cjmuli  10926  ipcni  10927  crrei  10929  crimi  10930  rexfiuz  10982  sqrt1  11039  sqrt4  11040  sqrt9  11041  abs1  11065  sqrtmulii  11127  abslti  11131  abslei  11132  abssubi  11143  absmuli  11144  sqabsaddi  11145  sqabssubi  11146  abstrii  11148  fimaxre2  11219  climz  11284  abscn2  11307  recn2  11309  imcn2  11310  climabs  11312  climre  11314  climim  11315  fsumcnv  11429  fsumrelem  11463  fsumre  11464  fsumim  11465  arisum2  11491  expcnv  11496  geo2sum2  11507  geo2lim  11508  0.999...  11513  geoihalfsum  11514  fprodcnv  11617  fprodge0  11629  fprodge1  11631  ege2le3  11663  ef0  11664  reeff1  11692  tan0  11723  ef01bndlem  11748  sin01bnd  11749  cos01bnd  11750  cos1bnd  11751  cos2bnd  11752  sin01gt0  11753  cos01gt0  11754  sin02gt0  11755  sincos1sgn  11756  sincos2sgn  11757  cos12dec  11759  egt2lt3  11771  epos  11772  ene1  11776  eap1  11777  3dvdsdec  11853  3dvds2dec  11854  odd2np1lem  11860  n2dvds1  11900  z4even  11904  ndvdsi  11921  flodddiv4  11922  gcd0val  11944  6gcd4e2  11979  3lcm2e6woprm  12069  6lcm4e12  12070  3lcm2e6  12143  sqrt2irrlem  12144  phimullem  12208  pockthi  12339  xpnnen  12378  xpomen  12379  ennnfonelemj0  12385  ennnfonelem0  12389  ennnfonelemhf1o  12397  exmidunben  12410  qnnen  12415  unct  12426  setscom  12485  strleun  12545  ismgm  12668  fn0g  12686  issgrp  12701  ismnddef  12711  isring  13009  mgpf  13020  txtopi  13428  txunii  13431  upxp  13439  uptx  13441  cnmpt1st  13455  cnmpt2nd  13456  txswaphmeolem  13487  qtopbasss  13688  cnmet  13697  cnopncntop  13704  remet  13707  blssioo  13712  tgqioo  13714  tgioo2cntop  13716  divcnap  13722  abscncf  13739  recncf  13740  imcncf  13741  cjcncf  13742  mulc1cncf  13743  cncfcn1cntop  13748  cdivcncfap  13754  expcncf  13759  cnrehmeocntop  13760  limccnp2lem  13812  limccnp2cntop  13813  dvcnp2cntop  13830  dvaddxxbr  13832  dvmulxxbr  13833  dvcoapbr  13838  dvrecap  13844  dveflem  13854  dvef  13855  sincn  13857  coscn  13858  reeff1oleme  13860  reeff1o  13861  cosz12  13868  sin0pilem1  13869  sin0pilem2  13870  pipos  13876  sinhalfpilem  13879  sincosq1lem  13913  sincosq1sgn  13914  sincosq2sgn  13915  sincosq3sgn  13916  sincosq4sgn  13917  sinq12gt0  13918  cosq14gt0  13920  cosq23lt0  13921  coseq0q4123  13922  coseq00topi  13923  coseq0negpitopi  13924  tangtx  13926  sincos4thpi  13928  tan4thpi  13929  sincos6thpi  13930  pigt3  13932  cosordlem  13937  cosq34lt1  13938  cos02pilt1  13939  cos0pilt1  13940  ioocosf1o  13942  negpitopissre  13943  log1  13954  loge  13955  2logb9irr  14056  sqrt2cxp2logb9e3  14060  2logb9irrap  14062  lgsdir2lem2  14097  lgsdir2lem3  14098  2sqlem9  14127  2sqlem10  14128  ex-fl  14133  ex-ceil  14134  ex-bc  14137  ex-dvds  14138  ex-gcd  14139  bj-charfunbi  14219  bj-unex  14327  bj-nn0suc0  14358  bj-nntrans  14359  bj-nnelirr  14361  012of  14401  2o01f  14402  pwle2  14404  nnsf  14410  peano3nninf  14412  exmidsbthrlem  14426  sbthom  14430  isomninnlem  14434  iooref1o  14438  trilpolemisumle  14442  trilpolemeq1  14444  trilpolemlt1  14445  apdiff  14452  iswomninnlem  14453  iswomni0  14455  ismkvnnlem  14456  dceqnconst  14463  dcapnconst  14464  nconstwlpolemgt0  14467  taupi  14474