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 )

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  443  mp3an23  1370  equs4  1777  sb4bor  1888  elvd  2826  eueq2dc  2999  sbcgf  3119  csbconstgf  3160  sbcnestg  3201  csbnestg  3202  csbnest1g  3203  ssindif0im  3583  mpteq1  4210  iinexgm  4285  exmid1stab  4340  mss  4361  eusv2nf  4597  eldifpw  4618  ordtriexmid  4663  onsucsssucexmid  4669  ordsucunielexmid  4673  nn0suc  4746  xpss1  4880  xpiindim  4912  reldm0  4994  elrnmpt1s  5027  resdm  5097  resid  5115  eliniseg  5152  trinxp  5176  inimasn  5200  ssrnres  5225  cnveq0  5239  coi2  5299  relrelss  5309  funcnvres  5449  funimaex  5461  fnresin1  5493  fnresin2  5494  fresin  5563  dffv3g  5686  ssimaex  5758  dmfco  5767  fvmpt  5776  fsn  5871  fsn2  5873  funop  5883  elabrex  5953  elabrexg  5954  f1elima  5969  2ndconst  6448  tposfun  6521  tpostpos2  6526  tfrexlem  6595  tfri3  6628  rdgruledefgg  6636  rdgss  6644  frecsuclem  6667  frecrdg  6669  oa0  6720  om0  6721  oei0  6722  oav2  6726  oa1suc  6730  nnmsucr  6751  nnm1  6788  nnm2  6789  ecelqsg  6852  ecidg  6863  xpider  6870  qsel  6876  mapdm0  6927  map0e  6957  mapsnconst  6966  ixpsnf1o  7008  map1  7091  dom1o  7106  xp1en  7111  xpcomco  7114  xpmapenlem  7139  findcard2s  7184  findcard2d  7185  findcard2sd  7186  exmidpw  7205  residfi  7244  fidcenumlemr  7262  sbthlem7  7270  eqinfti  7350  djueq1  7370  omp1eomlem  7424  endjusym  7426  eninl  7427  eninr  7428  difinfsn  7430  finomni  7470  pm54.43  7526  exmidonfinlem  7535  2onetap  7611  mulidpi  7675  nlt1pig  7698  indpi  7699  halfnqq  7767  archnqq  7774  prarloclemarch  7775  prarloclemarch2  7776  nnnq  7779  nq0a0  7814  addpinq1  7821  prarloclemlt  7850  prarloclemlo  7851  prarloclem3  7854  prarloclemcalc  7859  nqprm  7899  addnqpr1  7919  1idprl  7947  1idpru  7948  1idpr  7949  recexprlem1ssl  7990  recexprlem1ssu  7991  ltmprr  7999  0idsr  8124  1idsr  8125  00sr  8126  pn0sr  8128  negexsr  8129  recexgt0sr  8130  ltm1sr  8134  archsr  8139  prsrcl  8141  prsradd  8143  mappsrprg  8161  map2psrprg  8162  elrealeu  8186  pitonnlem1p1  8203  peano2nnnn  8210  ax1rid  8234  axcnre  8238  peano5nnnn  8249  peano2cn  8451  peano2re  8452  addlid  8455  subid  8535  subid1  8536  negid  8563  negeq0  8570  peano2cnm  8582  peano2rem  8583  mul01  8706  lt0neg1  8786  le0neg1  8788  recexre  8896  inelr  8902  rimul  8903  reapmul1  8913  apsqgt0  8919  mulge0  8937  negap0  8948  divvalap  8994  rerecclap  9050  div2negap  9055  divgt0i2i  9237  peano5nni  9286  nnge1  9306  times2  9412  addltmul  9521  nn0p1nn  9581  peano2nn0  9582  nn0lele2xi  9593  fcdmnn0supp  9594  fcdmnn0fsupp  9595  fcdmnn0suppg  9596  znnnlt1  9671  nn0lt10b  9705  prime  9724  msqznn  9725  zeo  9730  elnn1uz2  9986  qreccl  10021  qdivcl  10022  irrmul  10026  rphalfcl  10061  rpnegap  10066  zgt1rpn0n1  10075  ltpnf  10161  nltmnf  10169  pnfge  10170  xlt0neg1  10219  xle0neg1  10221  xaddpnf1  10227  xaddmnf1  10229  xaddid1  10243  xsubge0  10262  xleaddadd  10268  elioopnf  10348  elicopnf  10350  iccshftri  10376  iccshftli  10378  iccdili  10380  icccntri  10382  fzprval  10467  fzofzp1  10623  fzostep1  10634  flqge0nn0  10706  flqge1nn  10707  fldiv4p1lem1div2  10718  exp1  10960  qexpclz  10975  nn0sqcl  10981  expeq0  10985  expubnd  11011  sqval  11012  sqeq0  11017  resqcl  11022  zsqcl  11025  iexpcyc  11059  binom21  11067  bcnn  11173  bcn2  11180  bcn2p1  11187  bcnm1  11189  fihasheq0  11210  hashsng  11215  fihashen1  11216  fimaxq  11248  hashf1lem2  11264  iswrddm0  11306  ccatval2  11344  ccatsymb  11348  ccatrid  11353  eqs1  11374  s111  11377  swrdnd  11409  pfx00g  11425  shftfibg  11563  shftfib  11566  reim0  11604  imval2  11637  cjap0  11651  cjne0  11652  rexuz3  11734  resqrexlemover  11754  abssq  11825  nn0abscl  11829  nnabscl  11844  abs2dif  11850  max0addsup  11963  climshft  12048  bcxmas  12234  efgt1p2  12440  efgt1p  12441  efi4p  12462  resin4p  12463  recos4p  12464  sinbnd  12497  cosbnd  12498  dvdsval2  12535  zdvdsdc  12557  dvdsmul2  12559  dvdsmulcr  12566  dvdsabseq  12592  divconjdvds  12594  alzdvds  12599  fzo0dvdseq  12602  odd2np1lem  12617  mod2eq1n2dvds  12624  flodddiv4  12681  flodddiv4t2lthalf  12684  bits0  12693  bitsp1o  12698  gcdmndc  12710  gcd0id  12734  gcd1  12742  dfgcd2  12769  gcdmultiple  12775  gcdmultiplez  12776  dvdssq  12786  lcmmndc  12818  lcm0val  12821  dvdslcm  12825  lcmeq0  12827  lcmgcd  12834  lcmdvds  12835  lcmid  12836  lcm1  12837  cncongr2  12860  isprm3  12874  prm2orodd  12882  sqrt2irrap  12936  phiprm  12979  pc0  13061  pcxqcl  13069  pcdvdstr  13084  ballotfilem2  13206  ballotfilemfcc  13211  ballotfilem4  13219  unennn  13266  ennnfonelemim  13293  ctinfom  13297  ctinf  13299  enctlem  13301  elrestr  13578  tgval  13593  tgvalex  13594  xpsfrnel  13642  xpsfeq  13643  xpscf  13645  mulg1  13909  mulgnegnn  13912  ghmghmrn  14043  gsumconstcmn  14143  subrngintm  14493  subrgintm  14524  lsp0  14732  mulgrhm2  14917  zlmlemg  14935  zlmsca  14939  0opn  15030  topopn  15032  0cld  15136  ntropn  15141  ntrtop  15152  ntr0  15158  neipsm  15178  rest0  15203  xmetres  15406  metres  15407  mopnex  15529  tgioo  15578  cnlimcim  15695  cnlimc  15696  dvfre  15734  dveflem  15750  dvef  15751  efcn  15792  sin2pim  15837  cos2pim  15838  sinmpi  15839  cosmpi  15840  sinppi  15841  cosppi  15842  efimpi  15843  sincosq1lem  15849  sincosq2sgn  15851  sincosq3sgn  15852  sincosq4sgn  15853  sinq12gt0  15854  sinq34lt0t  15855  sincosq1eq  15863  abssinper  15870  logrpap0b  15900  loglt1b  15917  rpcxp0  15923  rpcxp1  15924  rpcxpsqrt  15947  logsqrt  15948  rprelogbdiv  15982  lgs0  16046  lgs2  16050  lgsneg  16057  lgsdilem  16060  lgsdir2lem2  16062  lgsdir2lem4  16064  lgsdir2lem5  16065  lgsne0  16071  2lgslem1a2  16120  2lgslem1c  16123  upgr0eop  16277  uspgrushgr  16335  usgruspgr  16338  usgr0eop  16397  0grsubgr  16419  wlklenvclwlk  16528  upgr2wlkdc  16532  clwwlk0on0  16586  konigsbergssiedgwen  16641  bj-inf2vnlem1  16910  pwle2  16942  pwf1oexmid  16943  domomsubct  16945  nninfsellemeqinf  16964  sbthom  16976  qdiff  17003  iswomninnlem  17004  redc0  17012