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  7360  djueq1  7380  omp1eomlem  7434  endjusym  7436  eninl  7437  eninr  7438  difinfsn  7440  finomni  7480  pm54.43  7536  exmidonfinlem  7545  2onetap  7621  mulidpi  7685  nlt1pig  7708  indpi  7709  halfnqq  7777  archnqq  7784  prarloclemarch  7785  prarloclemarch2  7786  nnnq  7789  nq0a0  7824  addpinq1  7831  prarloclemlt  7860  prarloclemlo  7861  prarloclem3  7864  prarloclemcalc  7869  nqprm  7909  addnqpr1  7929  1idprl  7957  1idpru  7958  1idpr  7959  recexprlem1ssl  8000  recexprlem1ssu  8001  ltmprr  8009  0idsr  8134  1idsr  8135  00sr  8136  pn0sr  8138  negexsr  8139  recexgt0sr  8140  ltm1sr  8144  archsr  8149  prsrcl  8151  prsradd  8153  mappsrprg  8171  map2psrprg  8172  elrealeu  8196  pitonnlem1p1  8213  peano2nnnn  8220  ax1rid  8244  axcnre  8248  peano5nnnn  8259  peano2cn  8462  peano2re  8463  addlid  8466  subid  8546  subid1  8547  negid  8574  negeq0  8581  peano2cnm  8593  peano2rem  8594  mul01  8717  lt0neg1  8797  le0neg1  8799  recexre  8908  inelr  8914  rimul  8915  reapmul1  8925  apsqgt0  8931  mulge0  8949  negap0  8960  divvalap  9006  rerecclap  9062  div2negap  9067  divgt0i2i  9249  indconst0  9304  indconst1  9305  peano5nni  9309  nnge1  9329  times2  9435  addltmul  9546  nn0p1nn  9606  peano2nn0  9607  nn0lele2xi  9618  fcdmnn0supp  9619  fcdmnn0fsupp  9620  fcdmnn0suppg  9621  znnnlt1  9696  nn0lt10b  9730  prime  9749  msqznn  9750  zeo  9755  elnn1uz2  10016  qreccl  10051  qdivcl  10052  irrmul  10057  rphalfcl  10092  rpnegap  10097  zgt1rpn0n1  10106  ltpnf  10192  nltmnf  10200  pnfge  10201  xlt0neg1  10250  xle0neg1  10252  xaddpnf1  10258  xaddmnf1  10260  xaddid1  10274  xsubge0  10293  xleaddadd  10299  elioopnf  10379  elicopnf  10381  iccshftri  10407  iccshftli  10409  iccdili  10411  icccntri  10413  fzprval  10499  fzofzp1  10655  fzostep1  10666  flqge0nn0  10741  flqge1nn  10742  fldiv4p1lem1div2  10753  exp1  10995  qexpclz  11010  nn0sqcl  11016  expeq0  11020  expubnd  11046  sqval  11047  sqeq0  11052  resqcl  11057  zsqcl  11060  iexpcyc  11094  binom21  11102  bcnn  11209  bcn2  11216  bcn2p1  11223  bcnm1  11225  fihasheq0  11246  hashsng  11251  fihashen1  11252  fimaxq  11284  hashf1lem2  11300  iswrddm0  11342  ccatval2  11380  ccatsymb  11384  ccatrid  11389  eqs1  11410  s111  11413  swrdnd  11445  pfx00g  11461  shftfibg  11599  shftfib  11602  reim0  11640  imval2  11673  cjap0  11687  cjne0  11688  rexuz3  11770  resqrexlemover  11790  abssq  11862  nn0abscl  11866  nnabscl  11881  abs2dif  11887  max0addsup  12000  climshft  12086  bcxmas  12272  efgt1p2  12478  efgt1p  12479  efi4p  12500  resin4p  12501  recos4p  12502  sinbnd  12535  cosbnd  12536  dvdsval2  12573  zdvdsdc  12595  dvdsmul2  12597  dvdsmulcr  12604  dvdsabseq  12630  divconjdvds  12632  alzdvds  12637  fzo0dvdseq  12640  odd2np1lem  12655  mod2eq1n2dvds  12662  flodddiv4  12719  flodddiv4t2lthalf  12722  bits0  12731  bitsp1o  12736  gcdmndc  12748  gcd0id  12772  gcd1  12780  dfgcd2  12807  gcdmultiple  12813  gcdmultiplez  12814  dvdssq  12824  lcmmndc  12856  lcm0val  12859  dvdslcm  12863  lcmeq0  12865  lcmgcd  12872  lcmdvds  12873  lcmid  12874  lcm1  12875  cncongr2  12898  isprm3  12912  prm2orodd  12920  sqrt2irrap  12976  phiprm  13021  pc0  13103  pcxqcl  13111  pcdvdstr  13126  ballotfilem2  13277  ballotfilemfcc  13282  ballotfilem4  13290  unennn  13337  ennnfonelemim  13364  ctinfom  13368  ctinf  13370  enctlem  13372  elrestr  13650  tgval  13665  tgvalex  13666  xpsfrnel  13714  xpsfeq  13715  xpscf  13717  mulg1  13981  mulgnegnn  13984  ghmghmrn  14115  gsumconstcmn  14215  subrngintm  14569  subrgintm  14600  lsp0  14809  mulgrhm2  14994  zlmlemg  15012  zlmsca  15016  0opn  15156  topopn  15158  0cld  15262  ntropn  15267  ntrtop  15278  ntr0  15284  neipsm  15304  rest0  15329  xmetres  15532  metres  15533  mopnex  15655  tgioo  15704  cnlimcim  15821  cnlimc  15822  dvfre  15860  dveflem  15876  dvef  15877  efcn  15918  efap1p  15929  sin2pim  15964  cos2pim  15965  sinmpi  15966  cosmpi  15967  sinppi  15968  cosppi  15969  efimpi  15970  sincosq1lem  15976  sincosq2sgn  15978  sincosq3sgn  15979  sincosq4sgn  15980  sinq12gt0  15981  sinq34lt0t  15982  sincosq1eq  15990  abssinper  15997  logrpap0b  16028  loglt1b  16045  rpcxp0  16053  rpcxp1  16054  rpcxpsqrt  16077  logsqrt  16078  rprelogbdiv  16112  ppiqp1le  16173  ppiqeq0  16182  ppiublem1  16192  ppiqub  16194  lgs0  16230  lgs2  16234  lgsneg  16241  lgsdilem  16244  lgsdir2lem2  16246  lgsdir2lem4  16248  lgsdir2lem5  16249  lgsne0  16255  2lgslem1a2  16304  2lgslem1c  16307  upgr0eop  16461  uspgrushgr  16519  usgruspgr  16522  usgr0eop  16581  0grsubgr  16603  wlklenvclwlk  16712  upgr2wlkdc  16716  clwwlk0on0  16770  konigsbergssiedgwen  16825  bj-inf2vnlem1  17094  pwle2  17126  pwf1oexmid  17127  domomsubct  17129  nninfsellemeqinf  17157  sbthom  17169  qdiff  17196  iswomninnlem  17197  redc0  17205