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  718  mp3an  1350  barbara  2153  eqeq12i  2220  el2v  2779  vtocl2  2830  spc2ev  2873  sbc2ie  3074  csbieb  3139  sseq12i  3225  uneq12i  3329  ineq12i  3376  ifssun  3590  nelpri  3662  ralpr  3693  rexpr  3694  preq12i  3720  dfop  3824  opeq12i  3830  breq12i  4060  mpteq2ia  4138  exmidundif  4258  exmidundifim  4259  opex  4281  opi2  4285  opth2  4292  opeqsn  4305  opeqpr  4306  uniop  4308  opelopaba  4320  braba  4321  opelopab  4326  brab  4327  opelopabaf  4328  unex  4496  snnex  4503  op1stb  4533  ifelpwun  4538  ifex  4541  onun2i  4547  onsucssi  4562  ontriexmidim  4578  ontr2exmid  4581  onsucsssucexmid  4583  onsucelsucexmid  4586  opthreg  4612  tfis  4639  finds  4656  finds2  4657  nnregexmid  4677  xpeq12i  4705  opelvv  4733  eqrelriiv  4777  eqrelrdv  4779  xpss  4791  xpex  4798  relop  4836  brco  4857  opelcnv  4868  brcnv  4869  asymref  5077  codir  5080  ssrnres  5134  dmprop  5166  dfco2  5191  cossxp  5214  cocnvss  5217  coex  5237  funsn  5331  fnsn  5337  feq23i  5430  resasplitss  5467  fabex  5476  fvex  5609  xpsn  5769  fmptap  5787  opabex  5821  acexmidlemv  5955  oveq12i  5969  oprabid  5989  oprabss  6044  caovcom  6117  opabex3  6220  iunex  6221  oprabex  6226  ofmres  6234  op1st  6245  op2nd  6246  fo1st  6256  fo2nd  6257  mpoex  6313  1stconst  6320  2ndconst  6321  algrflem  6328  dftpos4  6362  tpostpos  6363  tpossym  6375  frecex  6493  frecfnom  6500  sucinc  6544  fnoei  6551  oeiexg  6552  nnacli  6581  nnmcli  6582  elec  6674  ecovcom  6742  ecovass  6744  ecovdi  6746  fnmap  6755  mapval  6760  elmap  6777  elpm  6779  elpm2  6780  map0  6789  ixpconst  6808  entri  6891  endisj  6934  xpcomco  6936  phplem2  6965  ssfiexmid  6988  domfiexmid  6990  exmidpw2en  7024  unfiexmid  7030  unfiin  7038  inresflem  7177  casefun  7202  caserel  7204  caseinj  7206  omp1eomlem  7211  omp1eom  7212  endjusym  7213  djufun  7221  djuinj  7223  ctssdccl  7228  ctssdclemr  7229  nninfex  7238  infnninf  7241  fodjuomnilemdc  7261  ctssexmid  7267  exmidonfinlem  7317  dju1p1e2  7321  exmidfodomrlemr  7326  exmidfodomrlemrALT  7327  exmidaclem  7336  pw1dom2  7358  onntri35  7368  onntri45  7372  2oneel  7388  2omotaplemst  7390  acnccim  7404  1lt2pi  7473  indpi  7475  1nq  7499  rec1nq  7528  1lt2nq  7539  ltaddnq  7540  halfnqq  7543  prarloclemarch2  7552  prarloclemlt  7626  prarloclemcalc  7635  genpelxp  7644  ltexprlempr  7741  recexprlempr  7765  cauappcvgprlemcl  7786  cauappcvgprlemladd  7791  caucvgprlemcl  7809  caucvgprprlemcl  7837  suplocexprlemell  7846  suplocexprlemdisj  7853  suplocexprlemub  7856  0r  7883  1sr  7884  m1r  7885  m1p1sr  7893  m1m1sr  7894  0lt1sr  7898  1ne0sr  7899  1idsr  7901  recexgt0sr  7906  prsradd  7919  caucvgsrlemoffres  7933  caucvgsr  7935  mappsrprg  7937  map2psrprg  7938  pitonnlem1p1  7979  pitonnlem2  7980  pitoregt0  7982  peano2nnnn  7986  axi2m1  8008  axprecex  8013  axcnre  8014  nnindnn  8026  nntopi  8027  0cn  8084  addcli  8096  mulcli  8097  mulcomi  8098  readdcli  8105  remulcli  8106  rexpssxrxp  8137  ltrelxr  8153  gtneii  8188  lttri3i  8190  letri3i  8191  ltnsymi  8192  lenlti  8193  ltlei  8194  mulgt0i  8202  mulgt0ii  8203  0lt1  8219  addcomi  8236  pncan3oi  8308  resubcli  8355  subcli  8368  pncan3i  8369  negsubi  8370  subnegi  8371  subeq0i  8372  neg11i  8373  negcon1i  8374  negcon2i  8375  mulneg1i  8496  mulneg2i  8497  mul2negi  8498  addgt0ii  8584  ltnegi  8586  lenegi  8587  ltnegcon2i  8588  lesub0i  8589  ltaddposi  8590  posdifi  8591  ltnegcon1i  8592  lenegcon1i  8593  subge0i  8594  1ap0  8683  ltapii  8728  recrecapi  8837  dividapi  8838  div0api  8839  rec11apii  8854  divdiv32api  8860  recgt0ii  9000  ltrecii  9011  ltdiv23ii  9020  sup3exmid  9050  nnssre  9060  nnind  9072  nnmulcli  9078  nnsubi  9096  0le2  9146  1lt3  9228  2lt4  9230  1lt4  9231  3lt5  9233  2lt5  9234  1lt5  9235  4lt6  9237  3lt6  9238  2lt6  9239  1lt6  9240  5lt7  9242  4lt7  9243  3lt7  9244  2lt7  9245  1lt7  9246  6lt8  9248  5lt8  9249  4lt8  9250  3lt8  9251  2lt8  9252  1lt8  9253  7lt9  9255  6lt9  9256  5lt9  9257  4lt9  9258  3lt9  9259  2lt9  9260  1lt9  9261  2muline0  9282  nn0addcli  9352  nn0mulcli  9353  nn0addge1i  9363  nn0addge2i  9364  dfz2  9465  halfnz  9489  9p1e10  9526  numnncl  9533  numltc  9549  le9lt10  9550  nummac  9568  8lt10  9655  7lt10  9656  6lt10  9657  5lt10  9658  4lt10  9659  3lt10  9660  2lt10  9661  1lt10  9662  eluzaddi  9695  eluzsubi  9696  eluz2nn  9707  eluz4eluz2  9708  uzuzle23  9712  eluzge3nn  9713  divfnzn  9762  elq  9763  qreccl  9783  xrltnr  9921  mnfltpnf  9927  xaddmnf1  9990  pnfaddmnf  9992  mnfaddpnf  9993  xrex  9998  xaddid1  10004  xsubge0  10023  xposdif  10024  xleaddadd  10029  elicc2i  10081  ioomax  10090  iccmax  10091  ioopos  10092  elxrge0  10120  iccshftri  10137  iccshftli  10139  iccdili  10141  icccntri  10143  unitssre  10147  fz10  10188  fzpreddisj  10213  fz0to4untppr  10266  dfrp2  10428  fldiv4p1lem1div2  10470  fldiv4lem1div2  10472  frecfzennn  10593  xnn0nnen  10604  fnn0nninf  10605  fxnn0nninf  10606  0tonninf  10607  1tonninf  10608  m1expcl2  10728  m1expcl  10729  nn0expcli  10732  sqmuli  10789  cu2  10805  i3  10808  subsqi  10816  binom2subi  10822  bcpasc  10933  4bc2eq6  10941  hashinfom  10945  prhash2ex  10976  hashp1i  10977  lsw0g  11064  rei  11285  imi  11286  readdi  11314  imaddi  11315  remuli  11316  immuli  11317  cjaddi  11318  cjmuli  11319  ipcni  11320  crrei  11322  crimi  11323  rexfiuz  11375  sqrt1  11432  sqrt4  11433  sqrt9  11434  abs1  11458  sqrtmulii  11520  abslti  11524  abslei  11525  abssubi  11536  absmuli  11537  sqabsaddi  11538  sqabssubi  11539  abstrii  11541  fimaxre2  11613  climz  11678  abscn2  11701  recn2  11703  imcn2  11704  climabs  11706  climre  11708  climim  11709  fsumcnv  11823  fsumrelem  11857  fsumre  11858  fsumim  11859  arisum2  11885  expcnv  11890  geo2sum2  11901  geo2lim  11902  0.999...  11907  geoihalfsum  11908  fprodcnv  12011  fprodge0  12023  fprodge1  12025  ege2le3  12057  ef0  12058  reeff1  12086  tan0  12117  ef01bndlem  12142  sin01bnd  12143  cos01bnd  12144  cos1bnd  12145  cos2bnd  12146  sinltxirr  12147  sin01gt0  12148  cos01gt0  12149  sin02gt0  12150  sincos1sgn  12151  sincos2sgn  12152  cos12dec  12154  egt2lt3  12166  epos  12167  ene1  12171  eap1  12172  3dvds  12250  3dvdsdec  12251  3dvds2dec  12252  odd2np1lem  12258  n2dvds1  12298  z4even  12302  ndvdsi  12319  flodddiv4  12322  bitsp1o  12339  0bits  12345  gcd0val  12356  6gcd4e2  12391  3lcm2e6woprm  12483  6lcm4e12  12484  3lcm2e6  12557  sqrt2irrlem  12558  phimullem  12622  pockthi  12756  4sqlem19  12807  dec2dvds  12809  dec5dvds2  12811  dec2nprm  12813  modxai  12814  gcdi  12818  gcdmodi  12819  numexpp1  12822  karatsuba  12828  2exp7  12832  xpnnen  12840  xpomen  12841  ennnfonelemj0  12847  ennnfonelem0  12851  ennnfonelemhf1o  12859  exmidunben  12872  qnnen  12877  unct  12888  setscom  12947  strleun  13011  prdsex  13176  prdsvallem  13179  imasival  13213  ismgm  13264  fn0g  13282  fngsum  13295  issgrp  13310  ismnddef  13325  isghm  13654  isrng  13771  rngmgpf  13774  isring  13837  mgpf  13848  dfrhm2  13991  rhmex  13994  isdomn  14106  rmodislmod  14188  lidlmex  14312  mopnset  14389  cnfldstr  14395  cnfldcj  14402  cnfld0  14408  cnfldplusf  14411  zringcrng  14429  zringmulr  14436  zringmpg  14443  znval  14473  psrval  14503  fnpsr  14504  fnmpl  14530  txtopi  14808  txunii  14811  upxp  14819  uptx  14821  cnmpt1st  14835  cnmpt2nd  14836  txswaphmeolem  14867  qtopbasss  15068  cnmet  15077  cnfldms  15083  cnopncntop  15091  cnopn  15092  remet  15095  blssioo  15100  tgqioo  15102  tgioo2cntop  15104  tgioo2  15106  divcnap  15112  abscncf  15132  recncf  15133  imcncf  15134  cjcncf  15135  mulc1cncf  15136  cncfcn1cntop  15141  idcncf  15148  cdivcncfap  15151  expcncf  15156  cnrehmeocntop  15157  maxcncf  15162  mincncf  15163  ivthreinc  15192  hovercncf  15193  limccnp2lem  15223  limccnp2cntop  15224  dvcnp2cntop  15246  dvaddxxbr  15248  dvmulxxbr  15249  dvcoapbr  15254  dvrecap  15260  dveflem  15273  dvef  15274  sincn  15316  coscn  15317  reeff1oleme  15319  reeff1o  15320  cosz12  15327  sin0pilem1  15328  sin0pilem2  15329  pipos  15335  sinhalfpilem  15338  sincosq1lem  15372  sincosq1sgn  15373  sincosq2sgn  15374  sincosq3sgn  15375  sincosq4sgn  15376  sinq12gt0  15377  cosq14gt0  15379  cosq23lt0  15380  coseq0q4123  15381  coseq00topi  15382  coseq0negpitopi  15383  tangtx  15385  sincos4thpi  15387  tan4thpi  15388  sincos6thpi  15389  pigt3  15391  cosordlem  15396  cosq34lt1  15397  cos02pilt1  15398  cos0pilt1  15399  ioocosf1o  15401  negpitopissre  15402  log1  15413  loge  15414  2logb9irr  15518  sqrt2cxp2logb9e3  15522  2logb9irrap  15524  mpodvdsmulf1o  15537  fsumdvdsmul  15538  1sgm2ppw  15542  lgsdir2lem2  15581  lgsdir2lem3  15582  lgseisenlem4  15625  2lgsoddprmlem3  15663  2sqlem9  15676  2sqlem10  15677  opvtxfvi  15701  opiedgfvi  15702  umgrbien  15781  ex-fl  15800  ex-ceil  15801  ex-bc  15804  ex-dvds  15805  ex-gcd  15806  bj-charfunbi  15885  bj-unex  15993  bj-nn0suc0  16024  bj-nntrans  16025  bj-nnelirr  16027  012of  16069  2o01f  16070  pwle2  16076  nnsf  16083  peano3nninf  16085  exmidsbthrlem  16102  sbthom  16106  isomninnlem  16110  iooref1o  16114  trilpolemisumle  16118  trilpolemeq1  16120  trilpolemlt1  16121  apdiff  16128  iswomninnlem  16129  iswomni0  16131  ismkvnnlem  16132  dceqnconst  16140  dcapnconst  16141  nconstwlpolemgt0  16144  taupi  16153