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  3616  ralpr  3647  rexpr  3648  preq12i  3674  dfop  3777  opeq12i  3783  breq12i  4012  mpteq2ia  4089  exmidundif  4206  exmidundifim  4207  opex  4229  opi2  4233  opth2  4240  opeqsn  4252  opeqpr  4253  uniop  4255  opelopaba  4266  braba  4267  opelopab  4271  brab  4272  opelopabaf  4273  unex  4441  snnex  4448  op1stb  4478  ifelpwun  4483  onun2i  4490  onsucssi  4505  ontriexmidim  4521  ontr2exmid  4524  onsucsssucexmid  4526  onsucelsucexmid  4529  opthreg  4555  tfis  4582  finds  4599  finds2  4600  nnregexmid  4620  xpeq12i  4648  opelvv  4676  eqrelriiv  4720  eqrelrdv  4722  xpss  4734  xpex  4741  relop  4777  brco  4798  opelcnv  4809  brcnv  4810  asymref  5014  codir  5017  ssrnres  5071  dmprop  5103  dfco2  5128  cossxp  5151  cocnvss  5154  coex  5174  funsn  5264  fnsn  5270  feq23i  5360  resasplitss  5395  fabex  5404  fvex  5535  xpsn  5692  fmptap  5706  opabex  5740  acexmidlemv  5872  oveq12i  5886  oprabid  5906  oprabss  5960  caovcom  6031  opabex3  6122  iunex  6123  oprabex  6128  ofmres  6136  op1st  6146  op2nd  6147  fo1st  6157  fo2nd  6158  mpoex  6214  1stconst  6221  2ndconst  6222  algrflem  6229  dftpos4  6263  tpostpos  6264  tpossym  6276  frecex  6394  frecfnom  6401  sucinc  6445  fnoei  6452  oeiexg  6453  nnacli  6482  nnmcli  6483  elec  6573  ecovcom  6641  ecovass  6643  ecovdi  6645  fnmap  6654  mapval  6659  elmap  6676  elpm  6678  elpm2  6679  map0  6688  ixpconst  6707  entri  6785  endisj  6823  xpcomco  6825  phplem2  6852  ssfiexmid  6875  domfiexmid  6877  unfiexmid  6916  unfiin  6924  inresflem  7058  casefun  7083  caserel  7085  caseinj  7087  omp1eomlem  7092  omp1eom  7093  endjusym  7094  djufun  7102  djuinj  7104  ctssdccl  7109  ctssdclemr  7110  nninfex  7119  infnninf  7121  fodjuomnilemdc  7141  ctssexmid  7147  exmidonfinlem  7191  dju1p1e2  7195  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  exmidaclem  7206  pw1dom2  7225  onntri35  7235  onntri45  7239  2oneel  7254  2omotaplemst  7256  1lt2pi  7338  indpi  7340  1nq  7364  rec1nq  7393  1lt2nq  7404  ltaddnq  7405  halfnqq  7408  prarloclemarch2  7417  prarloclemlt  7491  prarloclemcalc  7500  genpelxp  7509  ltexprlempr  7606  recexprlempr  7630  cauappcvgprlemcl  7651  cauappcvgprlemladd  7656  caucvgprlemcl  7674  caucvgprprlemcl  7702  suplocexprlemell  7711  suplocexprlemdisj  7718  suplocexprlemub  7721  0r  7748  1sr  7749  m1r  7750  m1p1sr  7758  m1m1sr  7759  0lt1sr  7763  1ne0sr  7764  1idsr  7766  recexgt0sr  7771  prsradd  7784  caucvgsrlemoffres  7798  caucvgsr  7800  mappsrprg  7802  map2psrprg  7803  pitonnlem1p1  7844  pitonnlem2  7845  pitoregt0  7847  peano2nnnn  7851  axi2m1  7873  axprecex  7878  axcnre  7879  nnindnn  7891  nntopi  7892  0cn  7948  addcli  7960  mulcli  7961  mulcomi  7962  readdcli  7969  remulcli  7970  rexpssxrxp  8001  ltrelxr  8017  gtneii  8052  lttri3i  8054  letri3i  8055  ltnsymi  8056  lenlti  8057  ltlei  8058  mulgt0i  8066  mulgt0ii  8067  0lt1  8083  addcomi  8100  pncan3oi  8172  resubcli  8219  subcli  8232  pncan3i  8233  negsubi  8234  subnegi  8235  subeq0i  8236  neg11i  8237  negcon1i  8238  negcon2i  8239  mulneg1i  8360  mulneg2i  8361  mul2negi  8362  addgt0ii  8447  ltnegi  8449  lenegi  8450  ltnegcon2i  8451  lesub0i  8452  ltaddposi  8453  posdifi  8454  ltnegcon1i  8455  lenegcon1i  8456  subge0i  8457  1ap0  8546  ltapii  8591  recrecapi  8700  dividapi  8701  div0api  8702  rec11apii  8717  divdiv32api  8723  recgt0ii  8863  ltrecii  8874  ltdiv23ii  8883  sup3exmid  8913  nnssre  8922  nnind  8934  nnmulcli  8940  nnsubi  8958  0le2  9008  1lt3  9089  2lt4  9091  1lt4  9092  3lt5  9094  2lt5  9095  1lt5  9096  4lt6  9098  3lt6  9099  2lt6  9100  1lt6  9101  5lt7  9103  4lt7  9104  3lt7  9105  2lt7  9106  1lt7  9107  6lt8  9109  5lt8  9110  4lt8  9111  3lt8  9112  2lt8  9113  1lt8  9114  7lt9  9116  6lt9  9117  5lt9  9118  4lt9  9119  3lt9  9120  2lt9  9121  1lt9  9122  2muline0  9143  nn0addcli  9212  nn0mulcli  9213  nn0addge1i  9223  nn0addge2i  9224  dfz2  9324  halfnz  9348  9p1e10  9385  numnncl  9392  numltc  9408  le9lt10  9409  nummac  9427  8lt10  9514  7lt10  9515  6lt10  9516  5lt10  9517  4lt10  9518  3lt10  9519  2lt10  9520  1lt10  9521  eluzaddi  9553  eluzsubi  9554  eluz2nn  9565  eluz4eluz2  9566  uzuzle23  9570  eluzge3nn  9571  divfnzn  9620  elq  9621  qreccl  9641  xrltnr  9778  mnfltpnf  9784  xaddmnf1  9847  pnfaddmnf  9849  mnfaddpnf  9850  xrex  9855  xaddid1  9861  xsubge0  9880  xposdif  9881  xleaddadd  9886  elicc2i  9938  ioomax  9947  iccmax  9948  ioopos  9949  elxrge0  9977  iccshftri  9994  iccshftli  9996  iccdili  9998  icccntri  10000  unitssre  10004  fz10  10045  fzpreddisj  10070  fz0to4untppr  10123  dfrp2  10263  fldiv4p1lem1div2  10304  frecfzennn  10425  fnn0nninf  10436  fxnn0nninf  10437  0tonninf  10438  1tonninf  10439  m1expcl2  10541  m1expcl  10542  nn0expcli  10545  sqmuli  10602  cu2  10618  i3  10621  subsqi  10629  binom2subi  10635  bcpasc  10745  4bc2eq6  10753  hashinfom  10757  prhash2ex  10788  hashp1i  10789  rei  10907  imi  10908  readdi  10936  imaddi  10937  remuli  10938  immuli  10939  cjaddi  10940  cjmuli  10941  ipcni  10942  crrei  10944  crimi  10945  rexfiuz  10997  sqrt1  11054  sqrt4  11055  sqrt9  11056  abs1  11080  sqrtmulii  11142  abslti  11146  abslei  11147  abssubi  11158  absmuli  11159  sqabsaddi  11160  sqabssubi  11161  abstrii  11163  fimaxre2  11234  climz  11299  abscn2  11322  recn2  11324  imcn2  11325  climabs  11327  climre  11329  climim  11330  fsumcnv  11444  fsumrelem  11478  fsumre  11479  fsumim  11480  arisum2  11506  expcnv  11511  geo2sum2  11522  geo2lim  11523  0.999...  11528  geoihalfsum  11529  fprodcnv  11632  fprodge0  11644  fprodge1  11646  ege2le3  11678  ef0  11679  reeff1  11707  tan0  11738  ef01bndlem  11763  sin01bnd  11764  cos01bnd  11765  cos1bnd  11766  cos2bnd  11767  sin01gt0  11768  cos01gt0  11769  sin02gt0  11770  sincos1sgn  11771  sincos2sgn  11772  cos12dec  11774  egt2lt3  11786  epos  11787  ene1  11791  eap1  11792  3dvdsdec  11869  3dvds2dec  11870  odd2np1lem  11876  n2dvds1  11916  z4even  11920  ndvdsi  11937  flodddiv4  11938  gcd0val  11960  6gcd4e2  11995  3lcm2e6woprm  12085  6lcm4e12  12086  3lcm2e6  12159  sqrt2irrlem  12160  phimullem  12224  pockthi  12355  xpnnen  12394  xpomen  12395  ennnfonelemj0  12401  ennnfonelem0  12405  ennnfonelemhf1o  12413  exmidunben  12426  qnnen  12431  unct  12442  setscom  12501  strleun  12562  prdsex  12717  imasival  12726  ismgm  12775  fn0g  12793  issgrp  12808  ismnddef  12818  isring  13181  mgpf  13192  cnfldstr  13427  cnfldcj  13432  cnfld0  13435  cnfldplusf  13438  zringcrng  13452  zringmulr  13459  zringmpg  13466  txtopi  13731  txunii  13734  upxp  13742  uptx  13744  cnmpt1st  13758  cnmpt2nd  13759  txswaphmeolem  13790  qtopbasss  13991  cnmet  14000  cnopncntop  14007  remet  14010  blssioo  14015  tgqioo  14017  tgioo2cntop  14019  divcnap  14025  abscncf  14042  recncf  14043  imcncf  14044  cjcncf  14045  mulc1cncf  14046  cncfcn1cntop  14051  cdivcncfap  14057  expcncf  14062  cnrehmeocntop  14063  limccnp2lem  14115  limccnp2cntop  14116  dvcnp2cntop  14133  dvaddxxbr  14135  dvmulxxbr  14136  dvcoapbr  14141  dvrecap  14147  dveflem  14157  dvef  14158  sincn  14160  coscn  14161  reeff1oleme  14163  reeff1o  14164  cosz12  14171  sin0pilem1  14172  sin0pilem2  14173  pipos  14179  sinhalfpilem  14182  sincosq1lem  14216  sincosq1sgn  14217  sincosq2sgn  14218  sincosq3sgn  14219  sincosq4sgn  14220  sinq12gt0  14221  cosq14gt0  14223  cosq23lt0  14224  coseq0q4123  14225  coseq00topi  14226  coseq0negpitopi  14227  tangtx  14229  sincos4thpi  14231  tan4thpi  14232  sincos6thpi  14233  pigt3  14235  cosordlem  14240  cosq34lt1  14241  cos02pilt1  14242  cos0pilt1  14243  ioocosf1o  14245  negpitopissre  14246  log1  14257  loge  14258  2logb9irr  14359  sqrt2cxp2logb9e3  14363  2logb9irrap  14365  lgsdir2lem2  14400  lgsdir2lem3  14401  2lgsoddprmlem3  14429  2sqlem9  14441  2sqlem10  14442  ex-fl  14447  ex-ceil  14448  ex-bc  14451  ex-dvds  14452  ex-gcd  14453  bj-charfunbi  14533  bj-unex  14641  bj-nn0suc0  14672  bj-nntrans  14673  bj-nnelirr  14675  012of  14715  2o01f  14716  pwle2  14718  nnsf  14724  peano3nninf  14726  exmidsbthrlem  14740  sbthom  14744  isomninnlem  14748  iooref1o  14752  trilpolemisumle  14756  trilpolemeq1  14758  trilpolemlt1  14759  apdiff  14766  iswomninnlem  14767  iswomni0  14769  ismkvnnlem  14770  dceqnconst  14777  dcapnconst  14778  nconstwlpolemgt0  14781  taupi  14790