Theorem mpan2 417

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 413	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  mpanr12  431  mp3an23  1272  equs4  1667  sb4bor  1770  elvd  2638  eueq2dc  2802  sbcgf  2920  csbconstgf  2958  sbcnestg  2995  csbnestg  2996  csbnest1g  2997  ssindif0im  3361  mpteq1  3944  iinexgm  4011  mss  4077  eusv2nf  4306  eldifpw  4327  ordtriexmid  4366  onsucsssucexmid  4371  ordsucunielexmid  4375  nn0suc  4447  xpss1  4577  xpiindim  4604  reldm0  4685  elrnmpt1s  4717  resdm  4784  resid  4801  eliniseg  4835  trinxp  4858  inimasn  4882  ssrnres  4907  cnveq0  4921  coi2  4981  relrelss  4991  funcnvres  5121  funimaex  5133  fnresin1  5162  fnresin2  5163  fresin  5224  dffv3g  5336  ssimaex  5400  dmfco  5407  fvmpt  5416  fsn  5508  fsn2  5510  elabrex  5575  f1elima  5590  2ndconst  6025  tposfun  6063  tpostpos2  6068  tfrexlem  6137  tfri3  6170  rdgruledefgg  6178  rdgss  6186  frecsuclem  6209  frecrdg  6211  oa0  6258  om0  6259  oei0  6260  oav2  6264  oa1suc  6268  nnmsucr  6289  nnm1  6323  nnm2  6324  ecelqsg  6385  ecidg  6396  xpider  6403  qsel  6409  mapdm0  6460  map0e  6483  mapsnconst  6491  ixpsnf1o  6533  map1  6609  xp1en  6619  xpcomco  6622  xpmapenlem  6645  findcard2s  6686  findcard2d  6687  findcard2sd  6688  exmidpw  6704  fidcenumlemr  6744  sbthlem7  6752  eqinfti  6795  djueq1  6813  finomni  6883  pm54.43  6915  mulidpi  6974  nlt1pig  6997  indpi  6998  halfnqq  7066  archnqq  7073  prarloclemarch  7074  prarloclemarch2  7075  nnnq  7078  nq0a0  7113  addpinq1  7120  prarloclemlt  7149  prarloclemlo  7150  prarloclem3  7153  prarloclemcalc  7158  nqprm  7198  addnqpr1  7218  1idprl  7246  1idpru  7247  1idpr  7248  recexprlem1ssl  7289  recexprlem1ssu  7290  ltmprr  7298  0idsr  7410  1idsr  7411  00sr  7412  pn0sr  7414  negexsr  7415  recexgt0sr  7416  archsr  7424  prsrcl  7426  prsradd  7428  elrealeu  7464  pitonnlem1p1  7480  peano2nnnn  7487  ax1rid  7509  axcnre  7513  peano5nnnn  7524  peano2cn  7714  peano2re  7715  addid2  7718  subid  7798  subid1  7799  negid  7826  negeq0  7833  peano2cnm  7845  peano2rem  7846  mul01  7964  lt0neg1  8043  le0neg1  8045  recexre  8152  inelr  8158  rimul  8159  reapmul1  8169  apsqgt0  8175  mulge0  8193  negap0  8203  divvalap  8238  rerecclap  8294  div2negap  8299  divgt0i2i  8475  peano5nni  8523  nnge1  8543  times2  8643  addltmul  8750  nn0p1nn  8810  peano2nn0  8811  nn0lele2xi  8822  znnnlt1  8896  nn0lt10b  8925  prime  8944  msqznn  8945  zeo  8950  elnn1uz2  9193  qreccl  9226  qdivcl  9227  irrmul  9231  rphalfcl  9260  rpnegap  9265  ltpnf  9350  nltmnf  9357  pnfge  9358  xlt0neg1  9404  xle0neg1  9406  xaddpnf1  9412  xaddmnf1  9414  xaddid1  9428  xsubge0  9447  xleaddadd  9453  elioopnf  9533  elicopnf  9535  iccshftri  9561  iccshftli  9563  iccdili  9565  icccntri  9567  fzprval  9645  fzofzp1  9787  fzostep1  9797  flqge0nn0  9849  flqge1nn  9850  fldiv4p1lem1div2  9861  exp1  10076  qexpclz  10091  nn0sqcl  10097  expeq0  10101  expubnd  10127  sqval  10128  sqeq0  10133  resqcl  10137  zsqcl  10140  iexpcyc  10174  binom21  10181  bcnn  10280  bcn2  10287  bcn2p1  10293  bcnm1  10295  fihasheq0  10317  hashsng  10321  fihashen1  10322  fimaxq  10350  shftfibg  10369  shftfib  10372  reim0  10410  imval2  10443  cjap0  10456  cjne0  10457  rexuz3  10538  resqrexlemover  10558  abs00  10612  abssq  10629  nn0abscl  10633  nnabscl  10648  abs2dif  10654  max0addsup  10767  climshft  10847  bcxmas  11032  efgt1p2  11134  efgt1p  11135  efi4p  11157  resin4p  11158  recos4p  11159  sinbnd  11192  cosbnd  11193  dvdsval2  11226  zdvdsdc  11244  dvdsmul2  11246  dvdsmulcr  11253  dvdsabseq  11275  divconjdvds  11277  alzdvds  11282  fzo0dvdseq  11285  odd2np1lem  11299  mod2eq1n2dvds  11306  flodddiv4  11361  flodddiv4t2lthalf  11364  gcdmndc  11367  gcd0id  11397  gcd1  11405  dfgcd2  11430  gcdmultiple  11436  gcdmultiplez  11437  dvdssq  11447  lcmmndc  11471  lcm0val  11474  dvdslcm  11478  lcmeq0  11480  lcmgcd  11487  lcmdvds  11488  lcmid  11489  lcm1  11490  cncongr2  11513  isprm3  11527  prm2orodd  11535  sqrt2irrap  11585  phiprm  11626  unennn  11637  ressid  11704  elrestr  11812  0opn  11857  topopn  11859  tgval  11901  tgvalex  11902  0cld  11964  ntropn  11969  ntrtop  11980  ntr0  11986  neipsm  12006  rest0  12031  xmetres  12168  metres  12169  mopnex  12291  tgioo  12320  bj-inf2vnlem1  12573  nninfsellemeqinf  12613