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  2793  spc2ev  2834  sbc2ie  3035  csbieb  3099  sseq12i  3184  uneq12i  3288  ineq12i  3335  ifssun  3549  nelpri  3617  ralpr  3648  rexpr  3649  preq12i  3675  dfop  3778  opeq12i  3784  breq12i  4013  mpteq2ia  4090  exmidundif  4207  exmidundifim  4208  opex  4230  opi2  4234  opth2  4241  opeqsn  4253  opeqpr  4254  uniop  4256  opelopaba  4267  braba  4268  opelopab  4272  brab  4273  opelopabaf  4274  unex  4442  snnex  4449  op1stb  4479  ifelpwun  4484  onun2i  4491  onsucssi  4506  ontriexmidim  4522  ontr2exmid  4525  onsucsssucexmid  4527  onsucelsucexmid  4530  opthreg  4556  tfis  4583  finds  4600  finds2  4601  nnregexmid  4621  xpeq12i  4649  opelvv  4677  eqrelriiv  4721  eqrelrdv  4723  xpss  4735  xpex  4742  relop  4778  brco  4799  opelcnv  4810  brcnv  4811  asymref  5015  codir  5018  ssrnres  5072  dmprop  5104  dfco2  5129  cossxp  5152  cocnvss  5155  coex  5175  funsn  5265  fnsn  5271  feq23i  5361  resasplitss  5396  fabex  5405  fvex  5536  xpsn  5693  fmptap  5707  opabex  5741  acexmidlemv  5873  oveq12i  5887  oprabid  5907  oprabss  5961  caovcom  6032  opabex3  6123  iunex  6124  oprabex  6129  ofmres  6137  op1st  6147  op2nd  6148  fo1st  6158  fo2nd  6159  mpoex  6215  1stconst  6222  2ndconst  6223  algrflem  6230  dftpos4  6264  tpostpos  6265  tpossym  6277  frecex  6395  frecfnom  6402  sucinc  6446  fnoei  6453  oeiexg  6454  nnacli  6483  nnmcli  6484  elec  6574  ecovcom  6642  ecovass  6644  ecovdi  6646  fnmap  6655  mapval  6660  elmap  6677  elpm  6679  elpm2  6680  map0  6689  ixpconst  6708  entri  6786  endisj  6824  xpcomco  6826  phplem2  6853  ssfiexmid  6876  domfiexmid  6878  unfiexmid  6917  unfiin  6925  inresflem  7059  casefun  7084  caserel  7086  caseinj  7088  omp1eomlem  7093  omp1eom  7094  endjusym  7095  djufun  7103  djuinj  7105  ctssdccl  7110  ctssdclemr  7111  nninfex  7120  infnninf  7122  fodjuomnilemdc  7142  ctssexmid  7148  exmidonfinlem  7192  dju1p1e2  7196  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  exmidaclem  7207  pw1dom2  7226  onntri35  7236  onntri45  7240  2oneel  7255  2omotaplemst  7257  1lt2pi  7339  indpi  7341  1nq  7365  rec1nq  7394  1lt2nq  7405  ltaddnq  7406  halfnqq  7409  prarloclemarch2  7418  prarloclemlt  7492  prarloclemcalc  7501  genpelxp  7510  ltexprlempr  7607  recexprlempr  7631  cauappcvgprlemcl  7652  cauappcvgprlemladd  7657  caucvgprlemcl  7675  caucvgprprlemcl  7703  suplocexprlemell  7712  suplocexprlemdisj  7719  suplocexprlemub  7722  0r  7749  1sr  7750  m1r  7751  m1p1sr  7759  m1m1sr  7760  0lt1sr  7764  1ne0sr  7765  1idsr  7767  recexgt0sr  7772  prsradd  7785  caucvgsrlemoffres  7799  caucvgsr  7801  mappsrprg  7803  map2psrprg  7804  pitonnlem1p1  7845  pitonnlem2  7846  pitoregt0  7848  peano2nnnn  7852  axi2m1  7874  axprecex  7879  axcnre  7880  nnindnn  7892  nntopi  7893  0cn  7949  addcli  7961  mulcli  7962  mulcomi  7963  readdcli  7970  remulcli  7971  rexpssxrxp  8002  ltrelxr  8018  gtneii  8053  lttri3i  8055  letri3i  8056  ltnsymi  8057  lenlti  8058  ltlei  8059  mulgt0i  8067  mulgt0ii  8068  0lt1  8084  addcomi  8101  pncan3oi  8173  resubcli  8220  subcli  8233  pncan3i  8234  negsubi  8235  subnegi  8236  subeq0i  8237  neg11i  8238  negcon1i  8239  negcon2i  8240  mulneg1i  8361  mulneg2i  8362  mul2negi  8363  addgt0ii  8448  ltnegi  8450  lenegi  8451  ltnegcon2i  8452  lesub0i  8453  ltaddposi  8454  posdifi  8455  ltnegcon1i  8456  lenegcon1i  8457  subge0i  8458  1ap0  8547  ltapii  8592  recrecapi  8701  dividapi  8702  div0api  8703  rec11apii  8718  divdiv32api  8724  recgt0ii  8864  ltrecii  8875  ltdiv23ii  8884  sup3exmid  8914  nnssre  8923  nnind  8935  nnmulcli  8941  nnsubi  8959  0le2  9009  1lt3  9090  2lt4  9092  1lt4  9093  3lt5  9095  2lt5  9096  1lt5  9097  4lt6  9099  3lt6  9100  2lt6  9101  1lt6  9102  5lt7  9104  4lt7  9105  3lt7  9106  2lt7  9107  1lt7  9108  6lt8  9110  5lt8  9111  4lt8  9112  3lt8  9113  2lt8  9114  1lt8  9115  7lt9  9117  6lt9  9118  5lt9  9119  4lt9  9120  3lt9  9121  2lt9  9122  1lt9  9123  2muline0  9144  nn0addcli  9213  nn0mulcli  9214  nn0addge1i  9224  nn0addge2i  9225  dfz2  9325  halfnz  9349  9p1e10  9386  numnncl  9393  numltc  9409  le9lt10  9410  nummac  9428  8lt10  9515  7lt10  9516  6lt10  9517  5lt10  9518  4lt10  9519  3lt10  9520  2lt10  9521  1lt10  9522  eluzaddi  9554  eluzsubi  9555  eluz2nn  9566  eluz4eluz2  9567  uzuzle23  9571  eluzge3nn  9572  divfnzn  9621  elq  9622  qreccl  9642  xrltnr  9779  mnfltpnf  9785  xaddmnf1  9848  pnfaddmnf  9850  mnfaddpnf  9851  xrex  9856  xaddid1  9862  xsubge0  9881  xposdif  9882  xleaddadd  9887  elicc2i  9939  ioomax  9948  iccmax  9949  ioopos  9950  elxrge0  9978  iccshftri  9995  iccshftli  9997  iccdili  9999  icccntri  10001  unitssre  10005  fz10  10046  fzpreddisj  10071  fz0to4untppr  10124  dfrp2  10264  fldiv4p1lem1div2  10305  frecfzennn  10426  fnn0nninf  10437  fxnn0nninf  10438  0tonninf  10439  1tonninf  10440  m1expcl2  10542  m1expcl  10543  nn0expcli  10546  sqmuli  10603  cu2  10619  i3  10622  subsqi  10630  binom2subi  10636  bcpasc  10746  4bc2eq6  10754  hashinfom  10758  prhash2ex  10789  hashp1i  10790  rei  10908  imi  10909  readdi  10937  imaddi  10938  remuli  10939  immuli  10940  cjaddi  10941  cjmuli  10942  ipcni  10943  crrei  10945  crimi  10946  rexfiuz  10998  sqrt1  11055  sqrt4  11056  sqrt9  11057  abs1  11081  sqrtmulii  11143  abslti  11147  abslei  11148  abssubi  11159  absmuli  11160  sqabsaddi  11161  sqabssubi  11162  abstrii  11164  fimaxre2  11235  climz  11300  abscn2  11323  recn2  11325  imcn2  11326  climabs  11328  climre  11330  climim  11331  fsumcnv  11445  fsumrelem  11479  fsumre  11480  fsumim  11481  arisum2  11507  expcnv  11512  geo2sum2  11523  geo2lim  11524  0.999...  11529  geoihalfsum  11530  fprodcnv  11633  fprodge0  11645  fprodge1  11647  ege2le3  11679  ef0  11680  reeff1  11708  tan0  11739  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  cos1bnd  11767  cos2bnd  11768  sin01gt0  11769  cos01gt0  11770  sin02gt0  11771  sincos1sgn  11772  sincos2sgn  11773  cos12dec  11775  egt2lt3  11787  epos  11788  ene1  11792  eap1  11793  3dvdsdec  11870  3dvds2dec  11871  odd2np1lem  11877  n2dvds1  11917  z4even  11921  ndvdsi  11938  flodddiv4  11939  gcd0val  11961  6gcd4e2  11996  3lcm2e6woprm  12086  6lcm4e12  12087  3lcm2e6  12160  sqrt2irrlem  12161  phimullem  12225  pockthi  12356  xpnnen  12395  xpomen  12396  ennnfonelemj0  12402  ennnfonelem0  12406  ennnfonelemhf1o  12414  exmidunben  12427  qnnen  12432  unct  12443  setscom  12502  strleun  12563  prdsex  12718  imasival  12727  ismgm  12776  fn0g  12794  issgrp  12809  ismnddef  12819  isring  13183  mgpf  13194  rmodislmod  13441  cnfldstr  13460  cnfldcj  13465  cnfld0  13468  cnfldplusf  13471  zringcrng  13485  zringmulr  13492  zringmpg  13499  txtopi  13764  txunii  13767  upxp  13775  uptx  13777  cnmpt1st  13791  cnmpt2nd  13792  txswaphmeolem  13823  qtopbasss  14024  cnmet  14033  cnopncntop  14040  remet  14043  blssioo  14048  tgqioo  14050  tgioo2cntop  14052  divcnap  14058  abscncf  14075  recncf  14076  imcncf  14077  cjcncf  14078  mulc1cncf  14079  cncfcn1cntop  14084  cdivcncfap  14090  expcncf  14095  cnrehmeocntop  14096  limccnp2lem  14148  limccnp2cntop  14149  dvcnp2cntop  14166  dvaddxxbr  14168  dvmulxxbr  14169  dvcoapbr  14174  dvrecap  14180  dveflem  14190  dvef  14191  sincn  14193  coscn  14194  reeff1oleme  14196  reeff1o  14197  cosz12  14204  sin0pilem1  14205  sin0pilem2  14206  pipos  14212  sinhalfpilem  14215  sincosq1lem  14249  sincosq1sgn  14250  sincosq2sgn  14251  sincosq3sgn  14252  sincosq4sgn  14253  sinq12gt0  14254  cosq14gt0  14256  cosq23lt0  14257  coseq0q4123  14258  coseq00topi  14259  coseq0negpitopi  14260  tangtx  14262  sincos4thpi  14264  tan4thpi  14265  sincos6thpi  14266  pigt3  14268  cosordlem  14273  cosq34lt1  14274  cos02pilt1  14275  cos0pilt1  14276  ioocosf1o  14278  negpitopissre  14279  log1  14290  loge  14291  2logb9irr  14392  sqrt2cxp2logb9e3  14396  2logb9irrap  14398  lgsdir2lem2  14433  lgsdir2lem3  14434  2lgsoddprmlem3  14462  2sqlem9  14474  2sqlem10  14475  ex-fl  14480  ex-ceil  14481  ex-bc  14484  ex-dvds  14485  ex-gcd  14486  bj-charfunbi  14566  bj-unex  14674  bj-nn0suc0  14705  bj-nntrans  14706  bj-nnelirr  14708  012of  14748  2o01f  14749  pwle2  14751  nnsf  14757  peano3nninf  14759  exmidsbthrlem  14773  sbthom  14777  isomninnlem  14781  iooref1o  14785  trilpolemisumle  14789  trilpolemeq1  14791  trilpolemlt1  14792  apdiff  14799  iswomninnlem  14800  iswomni0  14802  ismkvnnlem  14803  dceqnconst  14810  dcapnconst  14811  nconstwlpolemgt0  14814  taupi  14823