Theorem mpan2 425

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 421	1 |- ( ph -> 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:  mpanr12  439  mp3an23  1340  equs4  1736  sb4bor  1846  elvd  2765  eueq2dc  2933  sbcgf  3053  csbconstgf  3093  sbcnestg  3134  csbnestg  3135  csbnest1g  3136  ssindif0im  3506  mpteq1  4113  iinexgm  4183  exmid1stab  4237  mss  4255  eusv2nf  4487  eldifpw  4508  ordtriexmid  4553  onsucsssucexmid  4559  ordsucunielexmid  4563  nn0suc  4636  xpss1  4769  xpiindim  4799  reldm0  4880  elrnmpt1s  4912  resdm  4981  resid  4999  eliniseg  5035  trinxp  5059  inimasn  5083  ssrnres  5108  cnveq0  5122  coi2  5182  relrelss  5192  funcnvres  5327  funimaex  5339  fnresin1  5368  fnresin2  5369  fresin  5432  dffv3g  5550  ssimaex  5618  dmfco  5625  fvmpt  5634  fsn  5730  fsn2  5732  elabrex  5800  elabrexg  5801  f1elima  5816  2ndconst  6275  tposfun  6313  tpostpos2  6318  tfrexlem  6387  tfri3  6420  rdgruledefgg  6428  rdgss  6436  frecsuclem  6459  frecrdg  6461  oa0  6510  om0  6511  oei0  6512  oav2  6516  oa1suc  6520  nnmsucr  6541  nnm1  6578  nnm2  6579  ecelqsg  6642  ecidg  6653  xpider  6660  qsel  6666  mapdm0  6717  map0e  6740  mapsnconst  6748  ixpsnf1o  6790  map1  6866  xp1en  6877  xpcomco  6880  xpmapenlem  6905  findcard2s  6946  findcard2d  6947  findcard2sd  6948  exmidpw  6964  residfi  6999  fidcenumlemr  7014  sbthlem7  7022  eqinfti  7079  djueq1  7099  omp1eomlem  7153  endjusym  7155  eninl  7156  eninr  7157  difinfsn  7159  finomni  7199  pm54.43  7250  exmidonfinlem  7253  2onetap  7315  mulidpi  7378  nlt1pig  7401  indpi  7402  halfnqq  7470  archnqq  7477  prarloclemarch  7478  prarloclemarch2  7479  nnnq  7482  nq0a0  7517  addpinq1  7524  prarloclemlt  7553  prarloclemlo  7554  prarloclem3  7557  prarloclemcalc  7562  nqprm  7602  addnqpr1  7622  1idprl  7650  1idpru  7651  1idpr  7652  recexprlem1ssl  7693  recexprlem1ssu  7694  ltmprr  7702  0idsr  7827  1idsr  7828  00sr  7829  pn0sr  7831  negexsr  7832  recexgt0sr  7833  ltm1sr  7837  archsr  7842  prsrcl  7844  prsradd  7846  mappsrprg  7864  map2psrprg  7865  elrealeu  7889  pitonnlem1p1  7906  peano2nnnn  7913  ax1rid  7937  axcnre  7941  peano5nnnn  7952  peano2cn  8154  peano2re  8155  addlid  8158  subid  8238  subid1  8239  negid  8266  negeq0  8273  peano2cnm  8285  peano2rem  8286  mul01  8408  lt0neg1  8487  le0neg1  8489  recexre  8597  inelr  8603  rimul  8604  reapmul1  8614  apsqgt0  8620  mulge0  8638  negap0  8649  divvalap  8693  rerecclap  8749  div2negap  8754  divgt0i2i  8936  peano5nni  8985  nnge1  9005  times2  9111  addltmul  9219  nn0p1nn  9279  peano2nn0  9280  nn0lele2xi  9291  znnnlt1  9365  nn0lt10b  9397  prime  9416  msqznn  9417  zeo  9422  elnn1uz2  9672  qreccl  9707  qdivcl  9708  irrmul  9712  rphalfcl  9747  rpnegap  9752  zgt1rpn0n1  9761  ltpnf  9846  nltmnf  9854  pnfge  9855  xlt0neg1  9904  xle0neg1  9906  xaddpnf1  9912  xaddmnf1  9914  xaddid1  9928  xsubge0  9947  xleaddadd  9953  elioopnf  10033  elicopnf  10035  iccshftri  10061  iccshftli  10063  iccdili  10065  icccntri  10067  fzprval  10148  fzofzp1  10294  fzostep1  10304  flqge0nn0  10362  flqge1nn  10363  fldiv4p1lem1div2  10374  exp1  10616  qexpclz  10631  nn0sqcl  10637  expeq0  10641  expubnd  10667  sqval  10668  sqeq0  10673  resqcl  10678  zsqcl  10681  iexpcyc  10715  binom21  10723  bcnn  10828  bcn2  10835  bcn2p1  10841  bcnm1  10843  fihasheq0  10864  hashsng  10869  fihashen1  10870  fimaxq  10898  iswrddm0  10938  shftfibg  10964  shftfib  10967  reim0  11005  imval2  11038  cjap0  11051  cjne0  11052  rexuz3  11134  resqrexlemover  11154  abssq  11225  nn0abscl  11229  nnabscl  11244  abs2dif  11250  max0addsup  11363  climshft  11447  bcxmas  11632  efgt1p2  11838  efgt1p  11839  efi4p  11860  resin4p  11861  recos4p  11862  sinbnd  11895  cosbnd  11896  dvdsval2  11933  zdvdsdc  11955  dvdsmul2  11957  dvdsmulcr  11964  dvdsabseq  11989  divconjdvds  11991  alzdvds  11996  fzo0dvdseq  11999  odd2np1lem  12013  mod2eq1n2dvds  12020  flodddiv4  12075  flodddiv4t2lthalf  12078  gcdmndc  12081  gcd0id  12116  gcd1  12124  dfgcd2  12151  gcdmultiple  12157  gcdmultiplez  12158  dvdssq  12168  lcmmndc  12200  lcm0val  12203  dvdslcm  12207  lcmeq0  12209  lcmgcd  12216  lcmdvds  12217  lcmid  12218  lcm1  12219  cncongr2  12242  isprm3  12256  prm2orodd  12264  sqrt2irrap  12318  phiprm  12361  pc0  12442  pcxqcl  12450  pcdvdstr  12465  unennn  12554  ennnfonelemim  12581  ctinfom  12585  ctinf  12587  enctlem  12589  elrestr  12858  tgval  12873  tgvalex  12874  xpsfrnel  12927  xpsfeq  12928  xpscf  12930  mulg1  13199  mulgnegnn  13202  ghmghmrn  13333  subrngintm  13708  subrgintm  13739  lsp0  13919  mulgrhm2  14098  zlmlemg  14116  zlmsca  14120  0opn  14174  topopn  14176  0cld  14280  ntropn  14285  ntrtop  14296  ntr0  14302  neipsm  14322  rest0  14347  xmetres  14550  metres  14551  mopnex  14673  tgioo  14714  cnlimcim  14825  cnlimc  14826  dvfre  14859  dveflem  14872  dvef  14873  efcn  14903  sin2pim  14948  cos2pim  14949  sinmpi  14950  cosmpi  14951  sinppi  14952  cosppi  14953  efimpi  14954  sincosq1lem  14960  sincosq2sgn  14962  sincosq3sgn  14963  sincosq4sgn  14964  sinq12gt0  14965  sinq34lt0t  14966  sincosq1eq  14974  abssinper  14981  logrpap0b  15011  loglt1b  15028  rpcxp0  15033  rpcxp1  15034  rpcxpsqrt  15056  logsqrt  15057  rprelogbdiv  15089  lgs0  15129  lgs2  15133  lgsneg  15140  lgsdilem  15143  lgsdir2lem2  15145  lgsdir2lem4  15147  lgsdir2lem5  15148  lgsne0  15154  bj-inf2vnlem1  15462  pwle2  15489  pwf1oexmid  15490  nninfsellemeqinf  15506  sbthom  15516  iswomninnlem  15539  redc0  15547