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  1319  barbara  2104  eqeq12i  2171  vtocl2  2767  spc2ev  2808  sbc2ie  3008  csbieb  3072  sseq12i  3156  uneq12i  3259  ineq12i  3306  ifssun  3519  nelpri  3584  ralpr  3614  rexpr  3615  preq12i  3641  dfop  3740  opeq12i  3746  breq12i  3974  mpteq2ia  4050  exmidundif  4167  exmidundifim  4168  opex  4189  opi2  4193  opth2  4200  opeqsn  4212  opeqpr  4213  uniop  4215  opelopaba  4226  braba  4227  opelopab  4231  brab  4232  opelopabaf  4233  unex  4400  snnex  4407  op1stb  4437  ifelpwun  4442  onun2i  4449  onsucssi  4464  ontriexmidim  4480  ontr2exmid  4483  onsucsssucexmid  4485  onsucelsucexmid  4488  opthreg  4514  tfis  4541  finds  4558  finds2  4559  nnregexmid  4579  xpeq12i  4607  opelvv  4635  eqrelriiv  4679  eqrelrdv  4681  xpss  4693  xpex  4700  relop  4735  brco  4756  opelcnv  4767  brcnv  4768  asymref  4970  codir  4973  ssrnres  5027  dmprop  5059  dfco2  5084  cossxp  5107  cocnvss  5110  coex  5130  funsn  5217  fnsn  5223  feq23i  5313  resasplitss  5348  fabex  5357  fvex  5487  xpsn  5642  fmptap  5656  opabex  5690  acexmidlemv  5819  oveq12i  5833  oprabid  5850  oprabss  5904  caovcom  5975  opabex3  6067  iunex  6068  oprabex  6073  ofmres  6081  op1st  6091  op2nd  6092  fo1st  6102  fo2nd  6103  mpoex  6158  1stconst  6165  2ndconst  6166  algrflem  6173  dftpos4  6207  tpostpos  6208  tpossym  6220  frecex  6338  frecfnom  6345  sucinc  6389  fnoei  6396  oeiexg  6397  nnacli  6426  nnmcli  6427  elec  6516  ecovcom  6584  ecovass  6586  ecovdi  6588  fnmap  6597  mapval  6602  elmap  6619  elpm  6621  elpm2  6622  map0  6631  ixpconst  6650  entri  6728  endisj  6766  xpcomco  6768  phplem2  6795  ssfiexmid  6818  domfiexmid  6820  unfiexmid  6859  unfiin  6867  inresflem  6998  casefun  7023  caserel  7025  caseinj  7027  omp1eomlem  7032  omp1eom  7033  endjusym  7034  djufun  7042  djuinj  7044  ctssdccl  7049  ctssdclemr  7050  nninfex  7059  infnninf  7061  fodjuomnilemdc  7081  ctssexmid  7087  exmidonfinlem  7122  dju1p1e2  7126  exmidfodomrlemr  7131  exmidfodomrlemrALT  7132  exmidaclem  7137  pw1dom2  7156  onntri35  7166  onntri45  7170  1lt2pi  7254  indpi  7256  1nq  7280  rec1nq  7309  1lt2nq  7320  ltaddnq  7321  halfnqq  7324  prarloclemarch2  7333  prarloclemlt  7407  prarloclemcalc  7416  genpelxp  7425  ltexprlempr  7522  recexprlempr  7546  cauappcvgprlemcl  7567  cauappcvgprlemladd  7572  caucvgprlemcl  7590  caucvgprprlemcl  7618  suplocexprlemell  7627  suplocexprlemdisj  7634  suplocexprlemub  7637  0r  7664  1sr  7665  m1r  7666  m1p1sr  7674  m1m1sr  7675  0lt1sr  7679  1ne0sr  7680  1idsr  7682  recexgt0sr  7687  prsradd  7700  caucvgsrlemoffres  7714  caucvgsr  7716  mappsrprg  7718  map2psrprg  7719  pitonnlem1p1  7760  pitonnlem2  7761  pitoregt0  7763  peano2nnnn  7767  axi2m1  7789  axprecex  7794  axcnre  7795  nnindnn  7807  nntopi  7808  0cn  7864  addcli  7876  mulcli  7877  mulcomi  7878  readdcli  7885  remulcli  7886  rexpssxrxp  7916  ltrelxr  7932  gtneii  7966  lttri3i  7968  letri3i  7969  ltnsymi  7970  lenlti  7971  ltlei  7972  mulgt0i  7980  mulgt0ii  7981  0lt1  7996  addcomi  8013  pncan3oi  8085  resubcli  8132  subcli  8145  pncan3i  8146  negsubi  8147  subnegi  8148  subeq0i  8149  neg11i  8150  negcon1i  8151  negcon2i  8152  mulneg1i  8273  mulneg2i  8274  mul2negi  8275  addgt0ii  8360  ltnegi  8362  lenegi  8363  ltnegcon2i  8364  lesub0i  8365  ltaddposi  8366  posdifi  8367  ltnegcon1i  8368  lenegcon1i  8369  subge0i  8370  1ap0  8459  ltapii  8504  recrecapi  8611  dividapi  8612  div0api  8613  rec11apii  8628  divdiv32api  8634  recgt0ii  8772  ltrecii  8783  ltdiv23ii  8792  sup3exmid  8822  nnssre  8831  nnind  8843  nnmulcli  8849  nnsubi  8867  0le2  8917  1lt3  8998  2lt4  9000  1lt4  9001  3lt5  9003  2lt5  9004  1lt5  9005  4lt6  9007  3lt6  9008  2lt6  9009  1lt6  9010  5lt7  9012  4lt7  9013  3lt7  9014  2lt7  9015  1lt7  9016  6lt8  9018  5lt8  9019  4lt8  9020  3lt8  9021  2lt8  9022  1lt8  9023  7lt9  9025  6lt9  9026  5lt9  9027  4lt9  9028  3lt9  9029  2lt9  9030  1lt9  9031  2muline0  9052  nn0addcli  9121  nn0mulcli  9122  nn0addge1i  9132  nn0addge2i  9133  dfz2  9230  halfnz  9254  9p1e10  9291  numnncl  9298  numltc  9314  le9lt10  9315  nummac  9333  8lt10  9420  7lt10  9421  6lt10  9422  5lt10  9423  4lt10  9424  3lt10  9425  2lt10  9426  1lt10  9427  eluzaddi  9459  eluzsubi  9460  eluz2nn  9471  eluz4eluz2  9472  uzuzle23  9476  eluzge3nn  9477  divfnzn  9523  elq  9524  qreccl  9544  xrltnr  9679  mnfltpnf  9685  xaddmnf1  9745  pnfaddmnf  9747  mnfaddpnf  9748  xrex  9753  xaddid1  9759  xsubge0  9778  xposdif  9779  xleaddadd  9784  elicc2i  9836  ioomax  9845  iccmax  9846  ioopos  9847  elxrge0  9875  iccshftri  9892  iccshftli  9894  iccdili  9896  icccntri  9898  unitssre  9902  fz10  9941  fzpreddisj  9966  dfrp2  10156  fldiv4p1lem1div2  10197  frecfzennn  10318  fnn0nninf  10329  fxnn0nninf  10330  0tonninf  10331  1tonninf  10332  m1expcl2  10434  m1expcl  10435  nn0expcli  10438  sqmuli  10494  cu2  10510  i3  10513  subsqi  10521  binom2subi  10526  bcpasc  10633  4bc2eq6  10641  hashinfom  10645  prhash2ex  10676  hashp1i  10677  rei  10792  imi  10793  readdi  10821  imaddi  10822  remuli  10823  immuli  10824  cjaddi  10825  cjmuli  10826  ipcni  10827  crrei  10829  crimi  10830  rexfiuz  10882  sqrt1  10939  sqrt4  10940  sqrt9  10941  abs1  10965  sqrtmulii  11027  abslti  11031  abslei  11032  abssubi  11043  absmuli  11044  sqabsaddi  11045  sqabssubi  11046  abstrii  11048  fimaxre2  11119  climz  11182  abscn2  11205  recn2  11207  imcn2  11208  climabs  11210  climre  11212  climim  11213  fsumcnv  11327  fsumrelem  11361  fsumre  11362  fsumim  11363  arisum2  11389  expcnv  11394  geo2sum2  11405  geo2lim  11406  0.999...  11411  geoihalfsum  11412  fprodcnv  11515  fprodge0  11527  fprodge1  11529  ege2le3  11561  ef0  11562  reeff1  11590  tan0  11621  ef01bndlem  11646  sin01bnd  11647  cos01bnd  11648  cos1bnd  11649  cos2bnd  11650  sin01gt0  11651  cos01gt0  11652  sin02gt0  11653  sincos1sgn  11654  sincos2sgn  11655  cos12dec  11657  egt2lt3  11669  epos  11670  ene1  11674  eap1  11675  3dvdsdec  11748  3dvds2dec  11749  odd2np1lem  11755  n2dvds1  11795  z4even  11799  ndvdsi  11816  flodddiv4  11817  gcd0val  11835  6gcd4e2  11870  3lcm2e6woprm  11954  6lcm4e12  11955  3lcm2e6  12025  sqrt2irrlem  12026  phimullem  12088  xpnnen  12106  xpomen  12107  ennnfonelemj0  12113  ennnfonelem0  12117  ennnfonelemhf1o  12125  exmidunben  12138  qnnen  12143  unct  12154  setscom  12201  strleun  12250  txtopi  12632  txunii  12635  upxp  12643  uptx  12645  cnmpt1st  12659  cnmpt2nd  12660  txswaphmeolem  12691  qtopbasss  12892  cnmet  12901  cnopncntop  12908  remet  12911  blssioo  12916  tgqioo  12918  tgioo2cntop  12920  divcnap  12926  abscncf  12943  recncf  12944  imcncf  12945  cjcncf  12946  mulc1cncf  12947  cncfcn1cntop  12952  cdivcncfap  12958  expcncf  12963  cnrehmeocntop  12964  limccnp2lem  13016  limccnp2cntop  13017  dvcnp2cntop  13034  dvaddxxbr  13036  dvmulxxbr  13037  dvcoapbr  13042  dvrecap  13048  dveflem  13058  dvef  13059  sincn  13061  coscn  13062  reeff1oleme  13064  reeff1o  13065  cosz12  13072  sin0pilem1  13073  sin0pilem2  13074  pipos  13080  sinhalfpilem  13083  sincosq1lem  13117  sincosq1sgn  13118  sincosq2sgn  13119  sincosq3sgn  13120  sincosq4sgn  13121  sinq12gt0  13122  cosq14gt0  13124  cosq23lt0  13125  coseq0q4123  13126  coseq00topi  13127  coseq0negpitopi  13128  tangtx  13130  sincos4thpi  13132  tan4thpi  13133  sincos6thpi  13134  pigt3  13136  cosordlem  13141  cosq34lt1  13142  cos02pilt1  13143  cos0pilt1  13144  ioocosf1o  13146  negpitopissre  13147  log1  13158  loge  13159  2logb9irr  13259  sqrt2cxp2logb9e3  13263  2logb9irrap  13265  ex-fl  13272  ex-ceil  13273  ex-bc  13276  ex-dvds  13277  ex-gcd  13278  bj-charfunbi  13357  bj-unex  13465  bj-nn0suc0  13496  bj-nntrans  13497  bj-nnelirr  13499  012of  13538  2o01f  13539  pwle2  13541  nnsf  13548  peano3nninf  13550  exmidsbthrlem  13564  sbthom  13568  isomninnlem  13572  iooref1o  13576  trilpolemisumle  13580  trilpolemeq1  13582  trilpolemlt1  13583  apdiff  13590  iswomninnlem  13591  iswomni0  13593  ismkvnnlem  13594  dceqnconst  13601  dcapnconst  13602  nconstwlpolemgt0  13605  taupi  13612