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  6535  tpostpos2  6540  tfrexlem  6609  tfri3  6642  rdgruledefgg  6650  rdgss  6658  frecsuclem  6681  frecrdg  6683  oa0  6734  om0  6735  oei0  6736  oav2  6740  oa1suc  6744  nnmsucr  6765  nnm1  6802  nnm2  6803  ecelqsg  6866  ecidg  6877  xpider  6884  qsel  6890  mapdm0  6941  map0e  6971  mapsnconst  6980  ixpsnf1o  7022  map1  7105  dom1o  7120  xp1en  7125  xpcomco  7128  xpmapenlem  7153  findcard2s  7198  findcard2d  7199  findcard2sd  7200  exmidpw  7219  residfi  7258  fidcenumlemr  7277  sbthlem7  7285  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  fcdmnn0fsupp  9627  fcdmnn0suppg  9628  znnnlt1  9703  nn0lt10b  9737  prime  9756  msqznn  9757  zeo  9762  elnn1uz2  10023  qreccl  10058  qdivcl  10059  irrmul  10064  rphalfcl  10099  rpnegap  10104  zgt1rpn0n1  10113  ltpnf  10199  nltmnf  10207  pnfge  10208  xlt0neg1  10257  xle0neg1  10259  xaddpnf1  10265  xaddmnf1  10267  xaddid1  10281  xsubge0  10300  xleaddadd  10306  elioopnf  10386  elicopnf  10388  iccshftri  10414  iccshftli  10416  iccdili  10418  icccntri  10420  fzprval  10506  fzofzp1  10662  fzostep1  10673  flqge0nn0  10749  flqge1nn  10750  fldiv4p1lem1div2  10761  exp1  11003  qexpclz  11018  nn0sqcl  11024  expeq0  11028  expubnd  11054  sqval  11055  sqeq0  11060  resqcl  11065  zsqcl  11068  iexpcyc  11102  binom21  11110  bcnn  11217  bcn2  11224  bcn2p1  11231  bcnm1  11233  fihasheq0  11254  hashsng  11259  fihashen1  11260  fimaxq  11292  hashf1lem2  11308  iswrddm0  11350  ccatval2  11388  ccatsymb  11392  ccatrid  11397  eqs1  11418  s111  11421  swrdnd  11453  pfx00g  11469  shftfibg  11607  shftfib  11610  reim0  11648  imval2  11681  cjap0  11695  cjne0  11696  rexuz3  11778  resqrexlemover  11798  abssq  11870  nn0abscl  11874  nnabscl  11889  abs2dif  11895  max0addsup  12008  climshft  12095  bcxmas  12281  efgt1p2  12487  efgt1p  12488  efi4p  12509  resin4p  12510  recos4p  12511  sinbnd  12544  cosbnd  12545  dvdsval2  12582  zdvdsdc  12604  dvdsmul2  12606  dvdsmulcr  12613  dvdsabseq  12639  divconjdvds  12641  alzdvds  12646  fzo0dvdseq  12649  odd2np1lem  12664  mod2eq1n2dvds  12671  flodddiv4  12728  flodddiv4t2lthalf  12731  bits0  12740  bitsp1o  12745  gcdmndc  12757  gcd0id  12781  gcd1  12789  dfgcd2  12816  gcdmultiple  12822  gcdmultiplez  12823  dvdssq  12833  lcmmndc  12865  lcm0val  12868  dvdslcm  12872  lcmeq0  12874  lcmgcd  12881  lcmdvds  12882  lcmid  12883  lcm1  12884  cncongr2  12907  isprm3  12921  prm2orodd  12929  sqrt2irrap  12985  phiprm  13030  pc0  13112  pcxqcl  13120  pcdvdstr  13135  ballotfilem2  13286  ballotfilemfcc  13291  ballotfilem4  13299  unennn  13346  ennnfonelemim  13373  ctinfom  13377  ctinf  13379  enctlem  13381  elrestr  13660  tgval  13675  tgvalex  13676  xpsfrnel  13724  xpsfeq  13725  xpscf  13727  mulg1  13991  mulgnegnn  13994  ghmghmrn  14125  cntrnsg  14176  gsumconstcmn  14266  subrngintm  14629  subrgintm  14660  lsp0  14869  mulgrhm2  15054  zlmlemg  15072  zlmsca  15076  0opn  15232  topopn  15234  0cld  15338  ntropn  15343  ntrtop  15354  ntr0  15360  neipsm  15380  rest0  15405  xmetres  15608  metres  15609  mopnex  15731  tgioo  15780  cnlimcim  15897  cnlimc  15898  dvfre  15936  dveflem  15952  dvef  15953  efcn  15994  efap1p  16005  sin2pim  16040  cos2pim  16041  sinmpi  16042  cosmpi  16043  sinppi  16044  cosppi  16045  efimpi  16046  sincosq1lem  16052  sincosq2sgn  16054  sincosq3sgn  16055  sincosq4sgn  16056  sinq12gt0  16057  sinq34lt0t  16058  sincosq1eq  16066  abssinper  16073  logrpap0b  16106  loglt1b  16123  rpcxp0  16131  rpcxp1  16132  rpcxpsqrt  16157  logsqrt  16158  rprelogbdiv  16193  ppiqp1le  16267  ppiqeq0  16280  ppiublem1  16291  ppiqub  16293  chtqub  16296  lgs0  16337  lgs2  16341  lgsneg  16348  lgsdilem  16351  lgsdir2lem2  16353  lgsdir2lem4  16355  lgsdir2lem5  16356  lgsne0  16362  2lgslem1a2  16411  2lgslem1c  16414  upgr0eop  16568  uspgrushgr  16626  usgruspgr  16629  usgr0eop  16688  0grsubgr  16710  wlklenvclwlk  16819  upgr2wlkdc  16823  clwwlk0on0  16877  konigsbergssiedgwen  16932  bj-inf2vnlem1  17201  pwle2  17233  pwf1oexmid  17234  domomsubct  17236  nninfsellemeqinf  17265  sbthom  17277  qdiff  17305  iswomninnlem  17306  redc0  17314