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  724  mp3an  1374  barbara  2178  eqeq12i  2245  el2v  2809  vtocl2  2860  spc2ev  2903  sbc2ie  3104  csbieb  3170  sseq12i  3256  uneq12i  3361  ineq12i  3408  ifssun  3624  nelpri  3697  ralpr  3728  rexpr  3729  preq12i  3757  dfop  3866  opeq12i  3872  breq12i  4102  mpteq2ia  4180  exmidundif  4302  exmidundifim  4303  opex  4327  opi2  4331  opth2  4338  opeqsn  4351  opeqpr  4352  uniop  4354  opelopaba  4366  braba  4367  opelopab  4372  brab  4373  opelopabaf  4374  unex  4544  snnex  4551  op1stb  4581  ifelpwun  4586  ifex  4589  onun2i  4595  onsucssi  4610  ontriexmidim  4626  ontr2exmid  4629  onsucsssucexmid  4631  onsucelsucexmid  4634  opthreg  4660  tfis  4687  finds  4704  finds2  4705  nnregexmid  4725  xpeq12i  4753  opelvv  4782  eqrelriiv  4826  eqrelrdv  4828  xpss  4840  xpex  4848  relop  4886  brco  4907  opelcnv  4918  brcnv  4919  asymref  5129  codir  5132  ssrnres  5186  dmprop  5218  dfco2  5243  cossxp  5266  cocnvss  5269  coex  5289  funsn  5385  fnsn  5391  feq23i  5484  resasplitss  5524  fabex  5533  fvex  5668  xpsn  5832  fmptap  5852  opabex  5888  acexmidlemv  6026  oveq12i  6040  oprabid  6060  oprabss  6117  caovcom  6190  opabex3  6293  iunex  6294  oprabex  6299  ofmres  6307  op1st  6318  op2nd  6319  fo1st  6329  fo2nd  6330  mpoex  6388  1stconst  6395  2ndconst  6396  algrflem  6403  dftpos4  6472  tpostpos  6473  tpossym  6485  frecex  6603  frecfnom  6610  2oex  6642  sucinc  6656  fnoei  6663  oeiexg  6664  nnacli  6693  nnmcli  6694  elec  6786  ecovcom  6854  ecovass  6856  ecovdi  6858  fnmap  6867  mapval  6872  elmap  6889  elpm  6891  elpm2  6892  map0  6901  ixpconst  6920  entri  7003  endisj  7051  xpcomco  7053  phplem2  7082  1ndom2  7094  ssfiexmid  7106  domfiexmid  7110  exmidpw2en  7147  unfiexmid  7153  unfiin  7161  inresflem  7302  casefun  7327  caserel  7329  caseinj  7331  omp1eomlem  7336  omp1eom  7337  endjusym  7338  djufun  7346  djuinj  7348  ctssdccl  7353  ctssdclemr  7354  nninfex  7363  infnninf  7366  fodjuomnilemdc  7386  ctssexmid  7392  exmidonfinlem  7447  dju1p1e2  7451  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  exmidaclem  7466  pw1dom2  7488  onntri35  7498  onntri45  7502  2oneel  7518  2omotaplemst  7520  acnccim  7534  1lt2pi  7603  indpi  7605  1nq  7629  rec1nq  7658  1lt2nq  7669  ltaddnq  7670  halfnqq  7673  prarloclemarch2  7682  prarloclemlt  7756  prarloclemcalc  7765  genpelxp  7774  ltexprlempr  7871  recexprlempr  7895  cauappcvgprlemcl  7916  cauappcvgprlemladd  7921  caucvgprlemcl  7939  caucvgprprlemcl  7967  suplocexprlemell  7976  suplocexprlemdisj  7983  suplocexprlemub  7986  0r  8013  1sr  8014  m1r  8015  m1p1sr  8023  m1m1sr  8024  0lt1sr  8028  1ne0sr  8029  1idsr  8031  recexgt0sr  8036  prsradd  8049  caucvgsrlemoffres  8063  caucvgsr  8065  mappsrprg  8067  map2psrprg  8068  pitonnlem1p1  8109  pitonnlem2  8110  pitoregt0  8112  peano2nnnn  8116  axi2m1  8138  axprecex  8143  axcnre  8144  nnindnn  8156  nntopi  8157  0cn  8214  addcli  8226  mulcli  8227  mulcomi  8228  readdcli  8235  remulcli  8236  rexpssxrxp  8266  ltrelxr  8282  gtneii  8317  lttri3i  8319  letri3i  8320  ltnsymi  8321  lenlti  8322  ltlei  8323  mulgt0i  8331  mulgt0ii  8332  0lt1  8348  addcomi  8365  pncan3oi  8437  resubcli  8484  subcli  8497  pncan3i  8498  negsubi  8499  subnegi  8500  subeq0i  8501  neg11i  8502  negcon1i  8503  negcon2i  8504  mulneg1i  8625  mulneg2i  8626  mul2negi  8627  addgt0ii  8713  ltnegi  8715  lenegi  8716  ltnegcon2i  8717  lesub0i  8718  ltaddposi  8719  posdifi  8720  ltnegcon1i  8721  lenegcon1i  8722  subge0i  8723  1ap0  8812  ltapii  8857  recrecapi  8966  dividapi  8967  div0api  8968  rec11apii  8983  divdiv32api  8989  recgt0ii  9129  ltrecii  9140  ltdiv23ii  9149  sup3exmid  9179  nnssre  9189  nnind  9201  nnmulcli  9207  nnsubi  9225  0le2  9275  1lt3  9357  2lt4  9359  1lt4  9360  3lt5  9362  2lt5  9363  1lt5  9364  4lt6  9366  3lt6  9367  2lt6  9368  1lt6  9369  5lt7  9371  4lt7  9372  3lt7  9373  2lt7  9374  1lt7  9375  6lt8  9377  5lt8  9378  4lt8  9379  3lt8  9380  2lt8  9381  1lt8  9382  7lt9  9384  6lt9  9385  5lt9  9386  4lt9  9387  3lt9  9388  2lt9  9389  1lt9  9390  2muline0  9411  nn0addcli  9481  nn0mulcli  9482  nn0addge1i  9492  nn0addge2i  9493  dfz2  9596  halfnz  9620  9p1e10  9657  numnncl  9664  numltc  9680  le9lt10  9681  nummac  9699  8lt10  9786  7lt10  9787  6lt10  9788  5lt10  9789  4lt10  9790  3lt10  9791  2lt10  9792  1lt10  9793  eluzaddi  9827  eluzsubi  9828  uzuzle23  9840  uzuzle24  9841  uzuzle34  9842  eluz2nn  9844  eluz4eluz2  9846  eluzge3nn  9850  divfnzn  9899  elq  9900  qreccl  9920  xrltnr  10058  mnfltpnf  10064  xaddmnf1  10127  pnfaddmnf  10129  mnfaddpnf  10130  xrex  10135  xaddid1  10141  xsubge0  10160  xposdif  10161  xleaddadd  10166  elicc2i  10218  ioomax  10227  iccmax  10228  ioopos  10229  elxrge0  10257  iccshftri  10274  iccshftli  10276  iccdili  10278  icccntri  10280  unitssre  10285  fz10  10326  fzpreddisj  10351  fz0to4untppr  10404  dfrp2  10569  fldiv4p1lem1div2  10611  fldiv4lem1div2  10613  frecfzennn  10734  xnn0nnen  10745  fnn0nninf  10746  fxnn0nninf  10747  0tonninf  10748  1tonninf  10749  m1expcl2  10869  m1expcl  10870  nn0expcli  10873  sqmuli  10930  cu2  10946  i3  10949  subsqi  10957  binom2subi  10963  bcpasc  11074  4bc2eq6  11082  hashinfom  11086  prhash2ex  11119  hashp1i  11120  lsw0g  11211  swrdccat3blem  11369  rei  11522  imi  11523  readdi  11551  imaddi  11552  remuli  11553  immuli  11554  cjaddi  11555  cjmuli  11556  ipcni  11557  crrei  11559  crimi  11560  rexfiuz  11612  sqrt1  11669  sqrt4  11670  sqrt9  11671  abs1  11695  sqrtmulii  11757  abslti  11761  abslei  11762  abssubi  11773  absmuli  11774  sqabsaddi  11775  sqabssubi  11776  abstrii  11778  fimaxre2  11850  climz  11915  abscn2  11938  recn2  11940  imcn2  11941  climabs  11943  climre  11945  climim  11946  fsumcnv  12061  fsumrelem  12095  fsumre  12096  fsumim  12097  arisum2  12123  expcnv  12128  geo2sum2  12139  geo2lim  12140  0.999...  12145  geoihalfsum  12146  fprodcnv  12249  fprodge0  12261  fprodge1  12263  ege2le3  12295  ef0  12296  reeff1  12324  tan0  12355  ef01bndlem  12380  sin01bnd  12381  cos01bnd  12382  cos1bnd  12383  cos2bnd  12384  sinltxirr  12385  sin01gt0  12386  cos01gt0  12387  sin02gt0  12388  sincos1sgn  12389  sincos2sgn  12390  cos12dec  12392  egt2lt3  12404  epos  12405  ene1  12409  eap1  12410  3dvds  12488  3dvdsdec  12489  3dvds2dec  12490  odd2np1lem  12496  n2dvds1  12536  z4even  12540  ndvdsi  12557  flodddiv4  12560  bitsp1o  12577  0bits  12583  gcd0val  12594  6gcd4e2  12629  3lcm2e6woprm  12721  6lcm4e12  12722  3lcm2e6  12795  sqrt2irrlem  12796  phimullem  12860  pockthi  12994  4sqlem19  13045  dec2dvds  13047  dec5dvds2  13049  dec2nprm  13051  modxai  13052  gcdi  13056  gcdmodi  13057  numexpp1  13060  karatsuba  13066  2exp7  13070  xpnnen  13078  xpomen  13079  ennnfonelemj0  13085  ennnfonelem0  13089  ennnfonelemhf1o  13097  exmidunben  13110  qnnen  13115  unct  13126  setscom  13185  strleun  13250  prdsex  13415  prdsvallem  13418  imasival  13452  ismgm  13503  fn0g  13521  fngsum  13534  issgrp  13549  ismnddef  13564  isghm  13893  isrng  14011  rngmgpf  14014  isring  14077  mgpf  14088  dfrhm2  14232  rhmex  14235  isdomn  14348  rmodislmod  14430  lidlmex  14554  mopnset  14631  cnfldstr  14637  cnfldcj  14644  cnfld0  14650  cnfldplusf  14653  zringcrng  14671  zringmulr  14678  zringmpg  14685  znval  14715  psrval  14745  fnpsr  14746  fnmpl  14777  txtopi  15055  txunii  15058  upxp  15066  uptx  15068  cnmpt1st  15082  cnmpt2nd  15083  txswaphmeolem  15114  qtopbasss  15315  cnmet  15324  cnfldms  15330  cnopncntop  15338  cnopn  15339  remet  15342  blssioo  15347  tgqioo  15349  tgioo2cntop  15351  tgioo2  15353  divcnap  15359  abscncf  15379  recncf  15380  imcncf  15381  cjcncf  15382  mulc1cncf  15383  cncfcn1cntop  15388  idcncf  15395  cdivcncfap  15398  expcncf  15403  cnrehmeocntop  15404  maxcncf  15409  mincncf  15410  ivthreinc  15439  hovercncf  15440  limccnp2lem  15470  limccnp2cntop  15471  dvcnp2cntop  15493  dvaddxxbr  15495  dvmulxxbr  15496  dvcoapbr  15501  dvrecap  15507  dveflem  15520  dvef  15521  sincn  15563  coscn  15564  reeff1oleme  15566  reeff1o  15567  cosz12  15574  sin0pilem1  15575  sin0pilem2  15576  pipos  15582  sinhalfpilem  15585  sincosq1lem  15619  sincosq1sgn  15620  sincosq2sgn  15621  sincosq3sgn  15622  sincosq4sgn  15623  sinq12gt0  15624  cosq14gt0  15626  cosq23lt0  15627  coseq0q4123  15628  coseq00topi  15629  coseq0negpitopi  15630  tangtx  15632  sincos4thpi  15634  tan4thpi  15635  sincos6thpi  15636  pigt3  15638  cosordlem  15643  cosq34lt1  15644  cos02pilt1  15645  cos0pilt1  15646  ioocosf1o  15648  negpitopissre  15649  log1  15660  loge  15661  2logb9irr  15765  sqrt2cxp2logb9e3  15769  2logb9irrap  15771  mpodvdsmulf1o  15787  fsumdvdsmul  15788  1sgm2ppw  15792  lgsdir2lem2  15831  lgsdir2lem3  15832  lgseisenlem4  15875  2lgsoddprmlem3  15913  2sqlem9  15926  2sqlem10  15927  opvtxfvi  15951  opiedgfvi  15952  umgrbien  16034  usgrprc  16176  vtxdfifiun  16221  upgr2wlkdc  16301  konigsbergvtx  16406  konigsbergiedg  16407  konigsbergumgr  16411  konigsberglem1  16412  konigsberglem2  16413  konigsberglem3  16414  konigsberglem5  16416  konigsberg  16417  ex-fl  16422  ex-ceil  16423  ex-bc  16426  ex-dvds  16427  ex-gcd  16428  bj-charfunbi  16510  bj-unex  16618  bj-nn0suc0  16649  bj-nntrans  16650  bj-nnelirr  16652  012of  16696  2o01f  16697  pwle2  16703  nnsf  16714  peano3nninf  16716  exmidsbthrlem  16733  sbthom  16737  repiecelem  16740  repiecele0  16741  repiecege0  16742  isomninnlem  16745  iooref1o  16749  trilpolemisumle  16753  trilpolemeq1  16755  trilpolemlt1  16756  apdiff  16763  iswomninnlem  16765  iswomni0  16767  ismkvnnlem  16768  dceqnconst  16776  dcapnconst  16777  nconstwlpolemgt0  16780  taupi  16789