Theorem mpan2 429

Description: An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

Hypotheses

Ref	Expression
mpan2.1	|- ps
mpan2.2	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
mpan2	|- ( ph -> ch )

Proof of Theorem mpan2

Step	Hyp	Ref	Expression
1		mpan2.1	. . 3 |- ps
2	1	a1i 9	. 2 |- ( ph -> ps )
3		mpan2.2	. 2 |- ( ( ph /\ ps ) -> ch )
4	2, 3	mpdan 425	1 |- ( ph -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mpanr12  443  mp3an23  1370  equs4  1777  sb4bor  1888  elvd  2826  eueq2dc  2999  sbcgf  3119  csbconstgf  3160  sbcnestg  3201  csbnestg  3202  csbnest1g  3203  ssindif0im  3584  mpteq1  4216  iinexgm  4292  exmid1stab  4347  mss  4368  eusv2nf  4604  eldifpw  4625  ordtriexmid  4670  onsucsssucexmid  4676  ordsucunielexmid  4680  nn0suc  4753  xpss1  4887  xpiindim  4919  reldm0  5001  elrnmpt1s  5034  resdm  5104  resid  5123  eliniseg  5160  trinxp  5184  inimasn  5208  ssrnres  5233  cnveq0  5247  coi2  5307  relrelss  5317  funcnvres  5457  funimaex  5469  fnresin1  5501  fnresin2  5502  fresin  5571  dffv3g  5694  ssimaex  5767  dmfco  5776  fvmpt  5785  fsn  5883  fsn2  5885  funop  5895  elabrex  5966  elabrexg  5967  f1elima  5982  2ndconst  6462  tposfun  6536  tpostpos2  6541  tfrexlem  6610  tfri3  6643  rdgruledefgg  6651  rdgss  6659  frecsuclem  6682  frecrdg  6684  oa0  6735  om0  6736  oei0  6737  oav2  6741  oa1suc  6745  nnmsucr  6766  nnm1  6803  nnm2  6804  ecelqsg  6867  ecidg  6878  xpider  6885  qsel  6891  mapdm0  6942  map0e  6972  mapsnconst  6982  ixpsnf1o  7024  map1  7107  dom1o  7122  xp1en  7127  xpcomco  7130  xpmapenlem  7155  findcard2s  7200  findcard2d  7201  findcard2sd  7202  exmidpw  7221  residfi  7260  fidcenumlemr  7279  sbthlem7  7287  eqinfti  7366  djueq1  7386  omp1eomlem  7440  endjusym  7442  eninl  7443  eninr  7444  difinfsn  7446  finomni  7486  pm54.43  7542  exmidonfinlem  7551  2onetap  7627  mulidpi  7691  nlt1pig  7714  indpi  7715  halfnqq  7783  archnqq  7790  prarloclemarch  7791  prarloclemarch2  7792  nnnq  7795  nq0a0  7830  addpinq1  7837  prarloclemlt  7866  prarloclemlo  7867  prarloclem3  7870  prarloclemcalc  7875  nqprm  7915  addnqpr1  7935  1idprl  7963  1idpru  7964  1idpr  7965  recexprlem1ssl  8006  recexprlem1ssu  8007  ltmprr  8015  0idsr  8140  1idsr  8141  00sr  8142  pn0sr  8144  negexsr  8145  recexgt0sr  8146  ltm1sr  8150  archsr  8155  prsrcl  8157  prsradd  8159  mappsrprg  8177  map2psrprg  8178  elrealeu  8202  pitonnlem1p1  8219  peano2nnnn  8226  ax1rid  8250  axcnre  8254  peano5nnnn  8265  peano2cn  8468  peano2re  8469  addlid  8472  subid  8552  subid1  8553  negid  8580  negeq0  8587  peano2cnm  8599  peano2rem  8600  mul01  8723  lt0neg1  8803  le0neg1  8805  recexre  8914  inelr  8920  rimul  8921  reapmul1  8931  apsqgt0  8937  mulge0  8955  negap0  8966  divvalap  9012  rerecclap  9068  div2negap  9073  divgt0i2i  9255  indconst0  9311  indconst1  9312  peano5nni  9316  nnge1  9336  times2  9442  addltmul  9553  nn0p1nn  9613  peano2nn0  9614  nn0lele2xi  9625  fcdmnn0supp  9626  fcdmnn0suppg  9627  znnnlt1  9701  nn0lt10b  9735  prime  9755  msqznn  9756  zeo  9761  elnn1uz2  10022  qreccl  10057  qdivcl  10058  irrmul  10063  rphalfcl  10098  rpnegap  10103  zgt1rpn0n1  10112  ltpnf  10198  nltmnf  10206  pnfge  10207  xlt0neg1  10256  xle0neg1  10258  xaddpnf1  10264  xaddmnf1  10266  xaddid1  10280  xsubge0  10299  xleaddadd  10305  elioopnf  10385  elicopnf  10387  iccshftri  10413  iccshftli  10415  iccdili  10417  icccntri  10419  fzprval  10505  fzofzp1  10661  fzostep1  10672  flqge0nn0  10748  flqge1nn  10749  fldiv4p1lem1div2  10760  exp1  11002  qexpclz  11017  nn0sqcl  11023  expeq0  11027  expubnd  11053  sqval  11054  sqeq0  11059  resqcl  11064  zsqcl  11067  iexpcyc  11101  binom21  11109  bcnn  11216  bcn2  11223  bcn2p1  11230  bcnm1  11232  fihasheq0  11253  hashsng  11258  fihashen1  11259  fimaxq  11291  hashf1lem2  11307  iswrddm0  11349  ccatval2  11387  ccatsymb  11391  ccatrid  11396  eqs1  11417  s111  11420  swrdnd  11452  pfx00g  11468  shftfibg  11606  shftfib  11609  reim0  11647  imval2  11680  cjap0  11694  cjne0  11695  rexuz3  11777  resqrexlemover  11797  abssq  11869  nn0abscl  11873  nnabscl  11888  abs2dif  11894  max0addsup  12007  climshft  12094  bcxmas  12280  efgt1p2  12486  efgt1p  12487  efi4p  12508  resin4p  12509  recos4p  12510  sinbnd  12543  cosbnd  12544  dvdsval2  12581  zdvdsdc  12603  dvdsmul2  12605  dvdsmulcr  12612  dvdsabseq  12638  divconjdvds  12640  alzdvds  12645  fzo0dvdseq  12648  odd2np1lem  12663  mod2eq1n2dvds  12670  flodddiv4  12727  flodddiv4t2lthalf  12730  bits0  12739  bitsp1o  12744  gcdmndc  12756  gcd0id  12780  gcd1  12788  dfgcd2  12815  gcdmultiple  12821  gcdmultiplez  12822  dvdssq  12832  lcmmndc  12864  lcm0val  12867  dvdslcm  12871  lcmeq0  12873  lcmgcd  12880  lcmdvds  12881  lcmid  12882  lcm1  12883  cncongr2  12906  isprm3  12920  prm2orodd  12928  sqrt2irrap  12984  phiprm  13029  pc0  13111  pcxqcl  13119  pcdvdstr  13134  ballotfilem2  13285  ballotfilemfcc  13290  ballotfilem4  13298  unennn  13345  ennnfonelemim  13372  ctinfom  13376  ctinf  13378  enctlem  13380  elrestr  13659  tgval  13674  tgvalex  13675  xpsfrnel  13723  xpsfeq  13724  xpscf  13726  mulg1  13990  mulgnegnn  13993  ghmghmrn  14124  cntrnsg  14175  gsumconstcmn  14265  subrngintm  14628  subrgintm  14659  lsp0  14868  mulgrhm2  15053  zlmlemg  15071  zlmsca  15075  0opn  15249  topopn  15251  0cld  15355  ntropn  15360  ntrtop  15371  ntr0  15377  neipsm  15397  rest0  15422  xmetres  15625  metres  15626  mopnex  15748  tgioo  15797  cnlimcim  15914  cnlimc  15915  dvfre  15953  dveflem  15969  dvef  15970  efcn  16011  efap1p  16022  sin2pim  16057  cos2pim  16058  sinmpi  16059  cosmpi  16060  sinppi  16061  cosppi  16062  efimpi  16063  sincosq1lem  16069  sincosq2sgn  16071  sincosq3sgn  16072  sincosq4sgn  16073  sinq12gt0  16074  sinq34lt0t  16075  sincosq1eq  16083  abssinper  16090  logrpap0b  16123  loglt1b  16140  rpcxp0  16148  rpcxp1  16149  rpcxpsqrt  16174  logsqrt  16175  rprelogbdiv  16210  ppiqp1le  16284  ppiqeq0  16297  ppiublem1  16308  ppiqub  16310  chtqub  16313  lgs0  16354  lgs2  16358  lgsneg  16365  lgsdilem  16368  lgsdir2lem2  16370  lgsdir2lem4  16372  lgsdir2lem5  16373  lgsne0  16379  2lgslem1a2  16428  2lgslem1c  16431  upgr0eop  16585  uspgrushgr  16643  usgruspgr  16646  usgr0eop  16705  0grsubgr  16727  wlklenvclwlk  16836  upgr2wlkdc  16840  clwwlk0on0  16894  konigsbergssiedgwen  16949  bj-inf2vnlem1  17218  pwle2  17250  pwf1oexmid  17251  domomsubct  17253  nninfsellemeqinf  17282  sbthom  17294  qdiff  17322  iswomninnlem  17323  redc0  17331