Theorem mp2an 418

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 416	. 2 |- ( ps -> ch )
5	1, 4	ax-mp 7	1 |- ch

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  mp4an  419  jaoi  672  mp3an  1274  barbara  2047  eqeq12i  2102  vtocl2  2677  spc2ev  2717  sbc2ie  2913  csbieb  2972  sseq12i  3055  uneq12i  3155  ineq12i  3202  nelpri  3476  ralpr  3503  rexpr  3504  preq12i  3530  dfop  3629  opeq12i  3635  breq12i  3862  mpteq2ia  3932  exmidundif  4045  exmidundifim  4046  opex  4067  opi2  4071  opth2  4078  opeqsn  4090  opeqpr  4091  uniop  4093  opelopaba  4104  braba  4105  opelopab  4109  brab  4110  opelopabaf  4111  unex  4278  snnex  4285  op1stb  4315  onun2i  4323  onsucssi  4338  ontr2exmid  4356  onsucsssucexmid  4358  onsucelsucexmid  4361  opthreg  4387  tfis  4413  finds  4430  finds2  4431  nnregexmid  4449  xpeq12i  4476  opelvv  4503  eqrelriiv  4547  eqrelrdv  4549  xpss  4561  xpex  4568  relop  4601  brco  4622  opelcnv  4633  brcnv  4634  asymref  4832  codir  4835  ssrnres  4888  dmprop  4920  dfco2  4945  cossxp  4968  cocnvss  4971  coex  4991  funsn  5077  fnsn  5083  feq23i  5171  resasplitss  5205  fabex  5214  fvex  5340  xpsn  5489  fmptap  5503  opabex  5537  acexmidlemv  5666  oveq12i  5680  oprabid  5697  oprabss  5750  caovcom  5818  opabex3  5909  iunex  5910  oprabex  5915  ofmres  5923  op1st  5933  op2nd  5934  fo1st  5944  fo2nd  5945  mpt2ex  5996  1stconst  6002  2ndconst  6003  algrflem  6010  dftpos4  6044  tpostpos  6045  tpossym  6057  frecex  6175  frecfnom  6182  sucinc  6222  fnoei  6229  oeiexg  6230  nnacli  6259  nnmcli  6260  elec  6347  ecovcom  6415  ecovass  6417  ecovdi  6419  fnmap  6428  mapval  6433  elmap  6450  elpm  6452  elpm2  6453  map0  6462  ixpconst  6481  entri  6559  endisj  6596  xpcomco  6598  phplem2  6625  ssfiexmid  6648  domfiexmid  6650  unfiexmid  6684  unfiin  6692  inresflem  6808  djuin  6812  casefun  6832  caserel  6834  caseinj  6836  djufun  6842  djuinj  6844  fodjuomnilemdc  6862  dju1p1e2  6886  exmidfodomrlemr  6891  exmidfodomrlemrALT  6892  1lt2pi  6962  indpi  6964  1nq  6988  rec1nq  7017  1lt2nq  7028  ltaddnq  7029  halfnqq  7032  prarloclemarch2  7041  prarloclemlt  7115  prarloclemcalc  7124  genpelxp  7133  ltexprlempr  7230  recexprlempr  7254  cauappcvgprlemcl  7275  cauappcvgprlemladd  7280  caucvgprlemcl  7298  caucvgprprlemcl  7326  0r  7359  1sr  7360  m1r  7361  m1p1sr  7369  m1m1sr  7370  0lt1sr  7374  1ne0sr  7375  1idsr  7377  recexgt0sr  7382  prsradd  7394  caucvgsrlemoffres  7408  caucvgsr  7410  pitonnlem1p1  7446  pitonnlem2  7447  pitoregt0  7449  peano2nnnn  7453  axi2m1  7473  axprecex  7478  axcnre  7479  nnindnn  7491  nntopi  7492  0cn  7543  addcli  7555  mulcli  7556  mulcomi  7557  readdcli  7564  remulcli  7565  rexpssxrxp  7595  ltrelxr  7610  gtneii  7643  lttri3i  7645  letri3i  7646  ltnsymi  7647  lenlti  7648  ltlei  7649  mulgt0i  7657  mulgt0ii  7658  0lt1  7673  addcomi  7689  pncan3oi  7761  resubcli  7808  subcli  7821  pncan3i  7822  negsubi  7823  subnegi  7824  subeq0i  7825  neg11i  7826  negcon1i  7827  negcon2i  7828  mulneg1i  7945  mulneg2i  7946  mul2negi  7947  addgt0ii  8032  ltnegi  8034  lenegi  8035  ltnegcon2i  8036  lesub0i  8037  ltaddposi  8038  posdifi  8039  ltnegcon1i  8040  lenegcon1i  8041  subge0i  8042  1ap0  8130  ltapii  8173  recrecapi  8274  dividapi  8275  div0api  8276  rec11apii  8291  divdiv32api  8297  recgt0ii  8431  ltrecii  8442  ltdiv23ii  8451  nnssre  8489  nnind  8501  nnmulcli  8507  nnsubi  8525  0le2  8575  1lt3  8650  2lt4  8652  1lt4  8653  3lt5  8655  2lt5  8656  1lt5  8657  4lt6  8659  3lt6  8660  2lt6  8661  1lt6  8662  5lt7  8664  4lt7  8665  3lt7  8666  2lt7  8667  1lt7  8668  6lt8  8670  5lt8  8671  4lt8  8672  3lt8  8673  2lt8  8674  1lt8  8675  7lt9  8677  6lt9  8678  5lt9  8679  4lt9  8680  3lt9  8681  2lt9  8682  1lt9  8683  2muline0  8704  nn0addcli  8773  nn0mulcli  8774  nn0addge1i  8784  nn0addge2i  8785  dfz2  8882  halfnz  8905  9p1e10  8942  numnncl  8949  numltc  8965  le9lt10  8966  nummac  8984  8lt10  9071  7lt10  9072  6lt10  9073  5lt10  9074  4lt10  9075  3lt10  9076  2lt10  9077  1lt10  9078  eluzaddi  9108  eluzsubi  9109  eluz2nn  9120  uzuzle23  9122  eluzge3nn  9123  divfnzn  9169  elq  9170  qreccl  9190  xrltnr  9313  mnfltpnf  9318  xrex  9368  elicc2i  9420  ioomax  9429  iccmax  9430  ioopos  9431  elxrge0  9459  iccshftri  9475  iccshftli  9477  iccdili  9479  icccntri  9481  unitssre  9485  fz10  9523  fzpreddisj  9548  fldiv4p1lem1div2  9775  frecfzennn  9896  fnn0nninf  9906  fxnn0nninf  9907  0tonninf  9908  1tonninf  9909  m1expcl2  10040  m1expcl  10041  nn0expcli  10044  sqmuli  10100  cu2  10116  i3  10119  subsqi  10127  binom2subi  10132  bcpasc  10237  4bc2eq6  10245  hashinfom  10249  prhash2ex  10280  hashp1i  10281  rei  10396  imi  10397  readdi  10425  imaddi  10426  remuli  10427  immuli  10428  cjaddi  10429  cjmuli  10430  ipcni  10431  crrei  10433  crimi  10434  rexfiuz  10485  sqrt1  10542  sqrt4  10543  sqrt9  10544  abs1  10568  sqrtmulii  10630  abslti  10634  abslei  10635  abssubi  10646  absmuli  10647  sqabsaddi  10648  sqabssubi  10649  abstrii  10651  fimaxre2  10721  climz  10743  abscn2  10766  recn2  10768  imcn2  10769  climabs  10771  climre  10773  climim  10774  fsumcnv  10894  fsumrelem  10928  fsumre  10929  fsumim  10930  arisum2  10956  expcnv  10961  geo2sum2  10972  geo2lim  10973  0.999...  10978  geoihalfsum  10979  ege2le3  11024  ef0  11025  reeff1  11054  tan0  11085  ef01bndlem  11110  sin01bnd  11111  cos01bnd  11112  cos1bnd  11113  cos2bnd  11114  sin01gt0  11115  cos01gt0  11116  sin02gt0  11117  sincos1sgn  11118  sincos2sgn  11119  egt2lt3  11130  epos  11131  ene1  11135  eap1  11136  3dvdsdec  11206  3dvds2dec  11207  odd2np1lem  11213  n2dvds1  11253  z4even  11257  ndvdsi  11274  flodddiv4  11275  gcd0val  11293  6gcd4e2  11325  3lcm2e6woprm  11409  6lcm4e12  11410  3lcm2e6  11480  sqrt2irrlem  11481  phimullem  11542  xpnnen  11548  xpomen  11549  setscom  11597  strleun  11646  abscncf  11945  recncf  11946  imcncf  11947  cjcncf  11948  mulc1cncf  11949  ex-fl  11956  ex-ceil  11957  ex-bc  11960  ex-dvds  11961  ex-gcd  11962  bj-unex  12114  bj-nn0suc0  12149  bj-nntrans  12150  bj-nnelirr  12152  pw1dom2  12193  nnsf  12198  peano3nninf  12200  nninfex  12204  exmidsbthrlem  12215