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  723  mp3an  1373  barbara  2178  eqeq12i  2245  el2v  2808  vtocl2  2859  spc2ev  2902  sbc2ie  3103  csbieb  3169  sseq12i  3255  uneq12i  3359  ineq12i  3406  ifssun  3620  nelpri  3693  ralpr  3724  rexpr  3725  preq12i  3753  dfop  3861  opeq12i  3867  breq12i  4097  mpteq2ia  4175  exmidundif  4296  exmidundifim  4297  opex  4321  opi2  4325  opth2  4332  opeqsn  4345  opeqpr  4346  uniop  4348  opelopaba  4360  braba  4361  opelopab  4366  brab  4367  opelopabaf  4368  unex  4538  snnex  4545  op1stb  4575  ifelpwun  4580  ifex  4583  onun2i  4589  onsucssi  4604  ontriexmidim  4620  ontr2exmid  4623  onsucsssucexmid  4625  onsucelsucexmid  4628  opthreg  4654  tfis  4681  finds  4698  finds2  4699  nnregexmid  4719  xpeq12i  4747  opelvv  4776  eqrelriiv  4820  eqrelrdv  4822  xpss  4834  xpex  4842  relop  4880  brco  4901  opelcnv  4912  brcnv  4913  asymref  5122  codir  5125  ssrnres  5179  dmprop  5211  dfco2  5236  cossxp  5259  cocnvss  5262  coex  5282  funsn  5378  fnsn  5384  feq23i  5477  resasplitss  5516  fabex  5525  fvex  5659  xpsn  5823  fmptap  5843  opabex  5877  acexmidlemv  6015  oveq12i  6029  oprabid  6049  oprabss  6106  caovcom  6179  opabex3  6283  iunex  6284  oprabex  6289  ofmres  6297  op1st  6308  op2nd  6309  fo1st  6319  fo2nd  6320  mpoex  6378  1stconst  6385  2ndconst  6386  algrflem  6393  dftpos4  6428  tpostpos  6429  tpossym  6441  frecex  6559  frecfnom  6566  2oex  6598  sucinc  6612  fnoei  6619  oeiexg  6620  nnacli  6649  nnmcli  6650  elec  6742  ecovcom  6810  ecovass  6812  ecovdi  6814  fnmap  6823  mapval  6828  elmap  6845  elpm  6847  elpm2  6848  map0  6857  ixpconst  6876  entri  6959  endisj  7007  xpcomco  7009  phplem2  7038  1ndom2  7050  ssfiexmid  7062  domfiexmid  7066  exmidpw2en  7103  unfiexmid  7109  unfiin  7117  inresflem  7258  casefun  7283  caserel  7285  caseinj  7287  omp1eomlem  7292  omp1eom  7293  endjusym  7294  djufun  7302  djuinj  7304  ctssdccl  7309  ctssdclemr  7310  nninfex  7319  infnninf  7322  fodjuomnilemdc  7342  ctssexmid  7348  exmidonfinlem  7403  dju1p1e2  7407  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  exmidaclem  7422  pw1dom2  7444  onntri35  7454  onntri45  7458  2oneel  7474  2omotaplemst  7476  acnccim  7490  1lt2pi  7559  indpi  7561  1nq  7585  rec1nq  7614  1lt2nq  7625  ltaddnq  7626  halfnqq  7629  prarloclemarch2  7638  prarloclemlt  7712  prarloclemcalc  7721  genpelxp  7730  ltexprlempr  7827  recexprlempr  7851  cauappcvgprlemcl  7872  cauappcvgprlemladd  7877  caucvgprlemcl  7895  caucvgprprlemcl  7923  suplocexprlemell  7932  suplocexprlemdisj  7939  suplocexprlemub  7942  0r  7969  1sr  7970  m1r  7971  m1p1sr  7979  m1m1sr  7980  0lt1sr  7984  1ne0sr  7985  1idsr  7987  recexgt0sr  7992  prsradd  8005  caucvgsrlemoffres  8019  caucvgsr  8021  mappsrprg  8023  map2psrprg  8024  pitonnlem1p1  8065  pitonnlem2  8066  pitoregt0  8068  peano2nnnn  8072  axi2m1  8094  axprecex  8099  axcnre  8100  nnindnn  8112  nntopi  8113  0cn  8170  addcli  8182  mulcli  8183  mulcomi  8184  readdcli  8191  remulcli  8192  rexpssxrxp  8223  ltrelxr  8239  gtneii  8274  lttri3i  8276  letri3i  8277  ltnsymi  8278  lenlti  8279  ltlei  8280  mulgt0i  8288  mulgt0ii  8289  0lt1  8305  addcomi  8322  pncan3oi  8394  resubcli  8441  subcli  8454  pncan3i  8455  negsubi  8456  subnegi  8457  subeq0i  8458  neg11i  8459  negcon1i  8460  negcon2i  8461  mulneg1i  8582  mulneg2i  8583  mul2negi  8584  addgt0ii  8670  ltnegi  8672  lenegi  8673  ltnegcon2i  8674  lesub0i  8675  ltaddposi  8676  posdifi  8677  ltnegcon1i  8678  lenegcon1i  8679  subge0i  8680  1ap0  8769  ltapii  8814  recrecapi  8923  dividapi  8924  div0api  8925  rec11apii  8940  divdiv32api  8946  recgt0ii  9086  ltrecii  9097  ltdiv23ii  9106  sup3exmid  9136  nnssre  9146  nnind  9158  nnmulcli  9164  nnsubi  9182  0le2  9232  1lt3  9314  2lt4  9316  1lt4  9317  3lt5  9319  2lt5  9320  1lt5  9321  4lt6  9323  3lt6  9324  2lt6  9325  1lt6  9326  5lt7  9328  4lt7  9329  3lt7  9330  2lt7  9331  1lt7  9332  6lt8  9334  5lt8  9335  4lt8  9336  3lt8  9337  2lt8  9338  1lt8  9339  7lt9  9341  6lt9  9342  5lt9  9343  4lt9  9344  3lt9  9345  2lt9  9346  1lt9  9347  2muline0  9368  nn0addcli  9438  nn0mulcli  9439  nn0addge1i  9449  nn0addge2i  9450  dfz2  9551  halfnz  9575  9p1e10  9612  numnncl  9619  numltc  9635  le9lt10  9636  nummac  9654  8lt10  9741  7lt10  9742  6lt10  9743  5lt10  9744  4lt10  9745  3lt10  9746  2lt10  9747  1lt10  9748  eluzaddi  9782  eluzsubi  9783  uzuzle23  9795  uzuzle24  9796  uzuzle34  9797  eluz2nn  9799  eluz4eluz2  9801  eluzge3nn  9805  divfnzn  9854  elq  9855  qreccl  9875  xrltnr  10013  mnfltpnf  10019  xaddmnf1  10082  pnfaddmnf  10084  mnfaddpnf  10085  xrex  10090  xaddid1  10096  xsubge0  10115  xposdif  10116  xleaddadd  10121  elicc2i  10173  ioomax  10182  iccmax  10183  ioopos  10184  elxrge0  10212  iccshftri  10229  iccshftli  10231  iccdili  10233  icccntri  10235  unitssre  10239  fz10  10280  fzpreddisj  10305  fz0to4untppr  10358  dfrp2  10522  fldiv4p1lem1div2  10564  fldiv4lem1div2  10566  frecfzennn  10687  xnn0nnen  10698  fnn0nninf  10699  fxnn0nninf  10700  0tonninf  10701  1tonninf  10702  m1expcl2  10822  m1expcl  10823  nn0expcli  10826  sqmuli  10883  cu2  10899  i3  10902  subsqi  10910  binom2subi  10916  bcpasc  11027  4bc2eq6  11035  hashinfom  11039  prhash2ex  11072  hashp1i  11073  lsw0g  11161  swrdccat3blem  11319  rei  11459  imi  11460  readdi  11488  imaddi  11489  remuli  11490  immuli  11491  cjaddi  11492  cjmuli  11493  ipcni  11494  crrei  11496  crimi  11497  rexfiuz  11549  sqrt1  11606  sqrt4  11607  sqrt9  11608  abs1  11632  sqrtmulii  11694  abslti  11698  abslei  11699  abssubi  11710  absmuli  11711  sqabsaddi  11712  sqabssubi  11713  abstrii  11715  fimaxre2  11787  climz  11852  abscn2  11875  recn2  11877  imcn2  11878  climabs  11880  climre  11882  climim  11883  fsumcnv  11997  fsumrelem  12031  fsumre  12032  fsumim  12033  arisum2  12059  expcnv  12064  geo2sum2  12075  geo2lim  12076  0.999...  12081  geoihalfsum  12082  fprodcnv  12185  fprodge0  12197  fprodge1  12199  ege2le3  12231  ef0  12232  reeff1  12260  tan0  12291  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  cos1bnd  12319  cos2bnd  12320  sinltxirr  12321  sin01gt0  12322  cos01gt0  12323  sin02gt0  12324  sincos1sgn  12325  sincos2sgn  12326  cos12dec  12328  egt2lt3  12340  epos  12341  ene1  12345  eap1  12346  3dvds  12424  3dvdsdec  12425  3dvds2dec  12426  odd2np1lem  12432  n2dvds1  12472  z4even  12476  ndvdsi  12493  flodddiv4  12496  bitsp1o  12513  0bits  12519  gcd0val  12530  6gcd4e2  12565  3lcm2e6woprm  12657  6lcm4e12  12658  3lcm2e6  12731  sqrt2irrlem  12732  phimullem  12796  pockthi  12930  4sqlem19  12981  dec2dvds  12983  dec5dvds2  12985  dec2nprm  12987  modxai  12988  gcdi  12992  gcdmodi  12993  numexpp1  12996  karatsuba  13002  2exp7  13006  xpnnen  13014  xpomen  13015  ennnfonelemj0  13021  ennnfonelem0  13025  ennnfonelemhf1o  13033  exmidunben  13046  qnnen  13051  unct  13062  setscom  13121  strleun  13186  prdsex  13351  prdsvallem  13354  imasival  13388  ismgm  13439  fn0g  13457  fngsum  13470  issgrp  13485  ismnddef  13500  isghm  13829  isrng  13946  rngmgpf  13949  isring  14012  mgpf  14023  dfrhm2  14167  rhmex  14170  isdomn  14282  rmodislmod  14364  lidlmex  14488  mopnset  14565  cnfldstr  14571  cnfldcj  14578  cnfld0  14584  cnfldplusf  14587  zringcrng  14605  zringmulr  14612  zringmpg  14619  znval  14649  psrval  14679  fnpsr  14680  fnmpl  14706  txtopi  14984  txunii  14987  upxp  14995  uptx  14997  cnmpt1st  15011  cnmpt2nd  15012  txswaphmeolem  15043  qtopbasss  15244  cnmet  15253  cnfldms  15259  cnopncntop  15267  cnopn  15268  remet  15271  blssioo  15276  tgqioo  15278  tgioo2cntop  15280  tgioo2  15282  divcnap  15288  abscncf  15308  recncf  15309  imcncf  15310  cjcncf  15311  mulc1cncf  15312  cncfcn1cntop  15317  idcncf  15324  cdivcncfap  15327  expcncf  15332  cnrehmeocntop  15333  maxcncf  15338  mincncf  15339  ivthreinc  15368  hovercncf  15369  limccnp2lem  15399  limccnp2cntop  15400  dvcnp2cntop  15422  dvaddxxbr  15424  dvmulxxbr  15425  dvcoapbr  15430  dvrecap  15436  dveflem  15449  dvef  15450  sincn  15492  coscn  15493  reeff1oleme  15495  reeff1o  15496  cosz12  15503  sin0pilem1  15504  sin0pilem2  15505  pipos  15511  sinhalfpilem  15514  sincosq1lem  15548  sincosq1sgn  15549  sincosq2sgn  15550  sincosq3sgn  15551  sincosq4sgn  15552  sinq12gt0  15553  cosq14gt0  15555  cosq23lt0  15556  coseq0q4123  15557  coseq00topi  15558  coseq0negpitopi  15559  tangtx  15561  sincos4thpi  15563  tan4thpi  15564  sincos6thpi  15565  pigt3  15567  cosordlem  15572  cosq34lt1  15573  cos02pilt1  15574  cos0pilt1  15575  ioocosf1o  15577  negpitopissre  15578  log1  15589  loge  15590  2logb9irr  15694  sqrt2cxp2logb9e3  15698  2logb9irrap  15700  mpodvdsmulf1o  15713  fsumdvdsmul  15714  1sgm2ppw  15718  lgsdir2lem2  15757  lgsdir2lem3  15758  lgseisenlem4  15801  2lgsoddprmlem3  15839  2sqlem9  15852  2sqlem10  15853  opvtxfvi  15877  opiedgfvi  15878  umgrbien  15960  usgrprc  16102  vtxdfifiun  16147  upgr2wlkdc  16227  ex-fl  16321  ex-ceil  16322  ex-bc  16325  ex-dvds  16326  ex-gcd  16327  bj-charfunbi  16406  bj-unex  16514  bj-nn0suc0  16545  bj-nntrans  16546  bj-nnelirr  16548  012of  16592  2o01f  16593  pwle2  16599  nnsf  16607  peano3nninf  16609  exmidsbthrlem  16626  sbthom  16630  isomninnlem  16634  iooref1o  16638  trilpolemisumle  16642  trilpolemeq1  16644  trilpolemlt1  16645  apdiff  16652  iswomninnlem  16653  iswomni0  16655  ismkvnnlem  16656  dceqnconst  16664  dcapnconst  16665  nconstwlpolemgt0  16668  taupi  16677