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  4215  iinexgm  4290  exmid1stab  4345  mss  4366  eusv2nf  4602  eldifpw  4623  ordtriexmid  4668  onsucsssucexmid  4674  ordsucunielexmid  4678  nn0suc  4751  xpss1  4885  xpiindim  4917  reldm0  4999  elrnmpt1s  5032  resdm  5102  resid  5120  eliniseg  5157  trinxp  5181  inimasn  5205  ssrnres  5230  cnveq0  5244  coi2  5304  relrelss  5314  funcnvres  5454  funimaex  5466  fnresin1  5498  fnresin2  5499  fresin  5568  dffv3g  5691  ssimaex  5764  dmfco  5773  fvmpt  5782  fsn  5880  fsn2  5882  funop  5892  elabrex  5963  elabrexg  5964  f1elima  5979  2ndconst  6458  tposfun  6531  tpostpos2  6536  tfrexlem  6605  tfri3  6638  rdgruledefgg  6646  rdgss  6654  frecsuclem  6677  frecrdg  6679  oa0  6730  om0  6731  oei0  6732  oav2  6736  oa1suc  6740  nnmsucr  6761  nnm1  6798  nnm2  6799  ecelqsg  6862  ecidg  6873  xpider  6880  qsel  6886  mapdm0  6937  map0e  6967  mapsnconst  6976  ixpsnf1o  7018  map1  7101  dom1o  7116  xp1en  7121  xpcomco  7124  xpmapenlem  7149  findcard2s  7194  findcard2d  7195  findcard2sd  7196  exmidpw  7215  residfi  7254  fidcenumlemr  7272  sbthlem7  7280  eqinfti  7361  djueq1  7381  omp1eomlem  7435  endjusym  7437  eninl  7438  eninr  7439  difinfsn  7441  finomni  7481  pm54.43  7537  exmidonfinlem  7546  2onetap  7622  mulidpi  7686  nlt1pig  7709  indpi  7710  halfnqq  7778  archnqq  7785  prarloclemarch  7786  prarloclemarch2  7787  nnnq  7790  nq0a0  7825  addpinq1  7832  prarloclemlt  7861  prarloclemlo  7862  prarloclem3  7865  prarloclemcalc  7870  nqprm  7910  addnqpr1  7930  1idprl  7958  1idpru  7959  1idpr  7960  recexprlem1ssl  8001  recexprlem1ssu  8002  ltmprr  8010  0idsr  8135  1idsr  8136  00sr  8137  pn0sr  8139  negexsr  8140  recexgt0sr  8141  ltm1sr  8145  archsr  8150  prsrcl  8152  prsradd  8154  mappsrprg  8172  map2psrprg  8173  elrealeu  8197  pitonnlem1p1  8214  peano2nnnn  8221  ax1rid  8245  axcnre  8249  peano5nnnn  8260  peano2cn  8463  peano2re  8464  addlid  8467  subid  8547  subid1  8548  negid  8575  negeq0  8582  peano2cnm  8594  peano2rem  8595  mul01  8718  lt0neg1  8798  le0neg1  8800  recexre  8909  inelr  8915  rimul  8916  reapmul1  8926  apsqgt0  8932  mulge0  8950  negap0  8961  divvalap  9007  rerecclap  9063  div2negap  9068  divgt0i2i  9250  indconst0  9305  indconst1  9306  peano5nni  9310  nnge1  9330  times2  9436  addltmul  9547  nn0p1nn  9607  peano2nn0  9608  nn0lele2xi  9619  fcdmnn0supp  9620  fcdmnn0fsupp  9621  fcdmnn0suppg  9622  znnnlt1  9697  nn0lt10b  9731  prime  9750  msqznn  9751  zeo  9756  elnn1uz2  10017  qreccl  10052  qdivcl  10053  irrmul  10058  rphalfcl  10093  rpnegap  10098  zgt1rpn0n1  10107  ltpnf  10193  nltmnf  10201  pnfge  10202  xlt0neg1  10251  xle0neg1  10253  xaddpnf1  10259  xaddmnf1  10261  xaddid1  10275  xsubge0  10294  xleaddadd  10300  elioopnf  10380  elicopnf  10382  iccshftri  10408  iccshftli  10410  iccdili  10412  icccntri  10414  fzprval  10500  fzofzp1  10656  fzostep1  10667  flqge0nn0  10743  flqge1nn  10744  fldiv4p1lem1div2  10755  exp1  10997  qexpclz  11012  nn0sqcl  11018  expeq0  11022  expubnd  11048  sqval  11049  sqeq0  11054  resqcl  11059  zsqcl  11062  iexpcyc  11096  binom21  11104  bcnn  11211  bcn2  11218  bcn2p1  11225  bcnm1  11227  fihasheq0  11248  hashsng  11253  fihashen1  11254  fimaxq  11286  hashf1lem2  11302  iswrddm0  11344  ccatval2  11382  ccatsymb  11386  ccatrid  11391  eqs1  11412  s111  11415  swrdnd  11447  pfx00g  11463  shftfibg  11601  shftfib  11604  reim0  11642  imval2  11675  cjap0  11689  cjne0  11690  rexuz3  11772  resqrexlemover  11792  abssq  11864  nn0abscl  11868  nnabscl  11883  abs2dif  11889  max0addsup  12002  climshft  12089  bcxmas  12275  efgt1p2  12481  efgt1p  12482  efi4p  12503  resin4p  12504  recos4p  12505  sinbnd  12538  cosbnd  12539  dvdsval2  12576  zdvdsdc  12598  dvdsmul2  12600  dvdsmulcr  12607  dvdsabseq  12633  divconjdvds  12635  alzdvds  12640  fzo0dvdseq  12643  odd2np1lem  12658  mod2eq1n2dvds  12665  flodddiv4  12722  flodddiv4t2lthalf  12725  bits0  12734  bitsp1o  12739  gcdmndc  12751  gcd0id  12775  gcd1  12783  dfgcd2  12810  gcdmultiple  12816  gcdmultiplez  12817  dvdssq  12827  lcmmndc  12859  lcm0val  12862  dvdslcm  12866  lcmeq0  12868  lcmgcd  12875  lcmdvds  12876  lcmid  12877  lcm1  12878  cncongr2  12901  isprm3  12915  prm2orodd  12923  sqrt2irrap  12979  phiprm  13024  pc0  13106  pcxqcl  13114  pcdvdstr  13129  ballotfilem2  13280  ballotfilemfcc  13285  ballotfilem4  13293  unennn  13340  ennnfonelemim  13367  ctinfom  13371  ctinf  13373  enctlem  13375  elrestr  13654  tgval  13669  tgvalex  13670  xpsfrnel  13718  xpsfeq  13719  xpscf  13721  mulg1  13985  mulgnegnn  13988  ghmghmrn  14119  cntrnsg  14170  gsumconstcmn  14250  subrngintm  14604  subrgintm  14635  lsp0  14844  mulgrhm2  15029  zlmlemg  15047  zlmsca  15051  0opn  15198  topopn  15200  0cld  15304  ntropn  15309  ntrtop  15320  ntr0  15326  neipsm  15346  rest0  15371  xmetres  15574  metres  15575  mopnex  15697  tgioo  15746  cnlimcim  15863  cnlimc  15864  dvfre  15902  dveflem  15918  dvef  15919  efcn  15960  efap1p  15971  sin2pim  16006  cos2pim  16007  sinmpi  16008  cosmpi  16009  sinppi  16010  cosppi  16011  efimpi  16012  sincosq1lem  16018  sincosq2sgn  16020  sincosq3sgn  16021  sincosq4sgn  16022  sinq12gt0  16023  sinq34lt0t  16024  sincosq1eq  16032  abssinper  16039  logrpap0b  16070  loglt1b  16087  rpcxp0  16095  rpcxp1  16096  rpcxpsqrt  16119  logsqrt  16120  rprelogbdiv  16154  ppiqp1le  16228  ppiqeq0  16241  ppiublem1  16252  ppiqub  16254  chtqub  16257  lgs0  16298  lgs2  16302  lgsneg  16309  lgsdilem  16312  lgsdir2lem2  16314  lgsdir2lem4  16316  lgsdir2lem5  16317  lgsne0  16323  2lgslem1a2  16372  2lgslem1c  16375  upgr0eop  16529  uspgrushgr  16587  usgruspgr  16590  usgr0eop  16649  0grsubgr  16671  wlklenvclwlk  16780  upgr2wlkdc  16784  clwwlk0on0  16838  konigsbergssiedgwen  16893  bj-inf2vnlem1  17162  pwle2  17194  pwf1oexmid  17195  domomsubct  17197  nninfsellemeqinf  17225  sbthom  17237  qdiff  17265  iswomninnlem  17266  redc0  17274