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  1366  equs4  1773  sb4bor  1883  elvd  2808  eueq2dc  2980  sbcgf  3100  csbconstgf  3141  sbcnestg  3182  csbnestg  3183  csbnest1g  3184  ssindif0im  3556  mpteq1  4178  iinexgm  4249  exmid1stab  4304  mss  4324  eusv2nf  4559  eldifpw  4580  ordtriexmid  4625  onsucsssucexmid  4631  ordsucunielexmid  4635  nn0suc  4708  xpss1  4842  xpiindim  4873  reldm0  4955  elrnmpt1s  4988  resdm  5058  resid  5076  eliniseg  5113  trinxp  5137  inimasn  5161  ssrnres  5186  cnveq0  5200  coi2  5260  relrelss  5270  funcnvres  5410  funimaex  5422  fnresin1  5454  fnresin2  5455  fresin  5523  dffv3g  5644  ssimaex  5716  dmfco  5723  fvmpt  5732  fsn  5827  fsn2  5829  funop  5839  elabrex  5908  elabrexg  5909  f1elima  5924  2ndconst  6396  tposfun  6469  tpostpos2  6474  tfrexlem  6543  tfri3  6576  rdgruledefgg  6584  rdgss  6592  frecsuclem  6615  frecrdg  6617  oa0  6668  om0  6669  oei0  6670  oav2  6674  oa1suc  6678  nnmsucr  6699  nnm1  6736  nnm2  6737  ecelqsg  6800  ecidg  6811  xpider  6818  qsel  6824  mapdm0  6875  map0e  6898  mapsnconst  6906  ixpsnf1o  6948  map1  7030  dom1o  7045  xp1en  7050  xpcomco  7053  xpmapenlem  7078  findcard2s  7122  findcard2d  7123  findcard2sd  7124  exmidpw  7143  residfi  7182  fidcenumlemr  7197  sbthlem7  7205  eqinfti  7279  djueq1  7299  omp1eomlem  7353  endjusym  7355  eninl  7356  eninr  7357  difinfsn  7359  finomni  7399  pm54.43  7455  exmidonfinlem  7464  2onetap  7534  mulidpi  7598  nlt1pig  7621  indpi  7622  halfnqq  7690  archnqq  7697  prarloclemarch  7698  prarloclemarch2  7699  nnnq  7702  nq0a0  7737  addpinq1  7744  prarloclemlt  7773  prarloclemlo  7774  prarloclem3  7777  prarloclemcalc  7782  nqprm  7822  addnqpr1  7842  1idprl  7870  1idpru  7871  1idpr  7872  recexprlem1ssl  7913  recexprlem1ssu  7914  ltmprr  7922  0idsr  8047  1idsr  8048  00sr  8049  pn0sr  8051  negexsr  8052  recexgt0sr  8053  ltm1sr  8057  archsr  8062  prsrcl  8064  prsradd  8066  mappsrprg  8084  map2psrprg  8085  elrealeu  8109  pitonnlem1p1  8126  peano2nnnn  8133  ax1rid  8157  axcnre  8161  peano5nnnn  8172  peano2cn  8373  peano2re  8374  addlid  8377  subid  8457  subid1  8458  negid  8485  negeq0  8492  peano2cnm  8504  peano2rem  8505  mul01  8627  lt0neg1  8707  le0neg1  8709  recexre  8817  inelr  8823  rimul  8824  reapmul1  8834  apsqgt0  8840  mulge0  8858  negap0  8869  divvalap  8913  rerecclap  8969  div2negap  8974  divgt0i2i  9156  peano5nni  9205  nnge1  9225  times2  9331  addltmul  9440  nn0p1nn  9500  peano2nn0  9501  nn0lele2xi  9512  fcdmnn0supp  9513  fcdmnn0suppg  9514  znnnlt1  9588  nn0lt10b  9621  prime  9640  msqznn  9641  zeo  9646  elnn1uz2  9902  qreccl  9937  qdivcl  9938  irrmul  9942  rphalfcl  9977  rpnegap  9982  zgt1rpn0n1  9991  ltpnf  10076  nltmnf  10084  pnfge  10085  xlt0neg1  10134  xle0neg1  10136  xaddpnf1  10142  xaddmnf1  10144  xaddid1  10158  xsubge0  10177  xleaddadd  10183  elioopnf  10263  elicopnf  10265  iccshftri  10291  iccshftli  10293  iccdili  10295  icccntri  10297  fzprval  10379  fzofzp1  10535  fzostep1  10546  flqge0nn0  10616  flqge1nn  10617  fldiv4p1lem1div2  10628  exp1  10870  qexpclz  10885  nn0sqcl  10891  expeq0  10895  expubnd  10921  sqval  10922  sqeq0  10927  resqcl  10932  zsqcl  10935  iexpcyc  10969  binom21  10977  bcnn  11082  bcn2  11089  bcn2p1  11095  bcnm1  11097  fihasheq0  11118  hashsng  11123  fihashen1  11124  fimaxq  11154  iswrddm0  11203  ccatval2  11241  ccatsymb  11245  ccatrid  11250  eqs1  11271  s111  11274  swrdnd  11306  pfx00g  11322  shftfibg  11460  shftfib  11463  reim0  11501  imval2  11534  cjap0  11547  cjne0  11548  rexuz3  11630  resqrexlemover  11650  abssq  11721  nn0abscl  11725  nnabscl  11740  abs2dif  11746  max0addsup  11859  climshft  11944  bcxmas  12130  efgt1p2  12336  efgt1p  12337  efi4p  12358  resin4p  12359  recos4p  12360  sinbnd  12393  cosbnd  12394  dvdsval2  12431  zdvdsdc  12453  dvdsmul2  12455  dvdsmulcr  12462  dvdsabseq  12488  divconjdvds  12490  alzdvds  12495  fzo0dvdseq  12498  odd2np1lem  12513  mod2eq1n2dvds  12520  flodddiv4  12577  flodddiv4t2lthalf  12580  bits0  12589  bitsp1o  12594  gcdmndc  12606  gcd0id  12630  gcd1  12638  dfgcd2  12665  gcdmultiple  12671  gcdmultiplez  12672  dvdssq  12682  lcmmndc  12714  lcm0val  12717  dvdslcm  12721  lcmeq0  12723  lcmgcd  12730  lcmdvds  12731  lcmid  12732  lcm1  12733  cncongr2  12756  isprm3  12770  prm2orodd  12778  sqrt2irrap  12832  phiprm  12875  pc0  12957  pcxqcl  12965  pcdvdstr  12980  unennn  13098  ennnfonelemim  13125  ctinfom  13129  ctinf  13131  enctlem  13133  elrestr  13410  tgval  13425  tgvalex  13426  xpsfrnel  13507  xpsfeq  13508  xpscf  13510  mulg1  13796  mulgnegnn  13799  ghmghmrn  13930  subrngintm  14307  subrgintm  14338  lsp0  14519  mulgrhm2  14706  zlmlemg  14724  zlmsca  14728  0opn  14817  topopn  14819  0cld  14923  ntropn  14928  ntrtop  14939  ntr0  14945  neipsm  14965  rest0  14990  xmetres  15193  metres  15194  mopnex  15316  tgioo  15365  cnlimcim  15482  cnlimc  15483  dvfre  15521  dveflem  15537  dvef  15538  efcn  15579  sin2pim  15624  cos2pim  15625  sinmpi  15626  cosmpi  15627  sinppi  15628  cosppi  15629  efimpi  15630  sincosq1lem  15636  sincosq2sgn  15638  sincosq3sgn  15639  sincosq4sgn  15640  sinq12gt0  15641  sinq34lt0t  15642  sincosq1eq  15650  abssinper  15657  logrpap0b  15687  loglt1b  15704  rpcxp0  15709  rpcxp1  15710  rpcxpsqrt  15733  logsqrt  15734  rprelogbdiv  15768  lgs0  15832  lgs2  15836  lgsneg  15843  lgsdilem  15846  lgsdir2lem2  15848  lgsdir2lem4  15850  lgsdir2lem5  15851  lgsne0  15857  2lgslem1a2  15906  2lgslem1c  15909  upgr0eop  16063  uspgrushgr  16121  usgruspgr  16124  usgr0eop  16183  0grsubgr  16205  wlklenvclwlk  16314  upgr2wlkdc  16318  clwwlk0on0  16372  konigsbergssiedgwen  16427  bj-inf2vnlem1  16686  pwle2  16720  pwf1oexmid  16721  domomsubct  16723  nninfsellemeqinf  16742  sbthom  16754  qdiff  16781  iswomninnlem  16782  redc0  16790