Theorem mp1i 10

Description: Drop and replace an antecedent. (Contributed by Stefan O'Rear, 29-Jan-2015.)

Hypotheses

Ref	Expression
mp1i.a	|- ph
mp1i.b	|- ( ph -> ps )

Assertion

Ref	Expression
mp1i	|- ( ch -> ps )

Proof of Theorem mp1i

Step	Hyp	Ref	Expression
1		mp1i.a	. . 3 |- ph
2		mp1i.b	. . 3 |- ( ph -> ps )
3	1, 2	ax-mp 5	. 2 |- ps
4	3	a1i 9	1 |- ( ch -> ps )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6

This theorem is referenced by:  poirr2  5120  relcoi2  5258  tfrlemi14d  6477  tfri1dALT  6495  mapsncnv  6840  findcard2d  7049  findcard2sd  7050  ac6sfi  7056  xpfi  7090  fifo  7143  updjudhcoinlf  7243  updjudhcoinrg  7244  updjud  7245  casefun  7248  omp1eomlem  7257  difinfsnlem  7262  djufun  7267  ctm  7272  ismkvnex  7318  cauappcvgprlemladd  7841  caucvgprprlemmu  7878  caucvgsrlemfv  7974  recidpirqlemcalc  8040  recidpirq  8041  axaddf  8051  axmulf  8052  xaddpnf1  10038  fldiv4lem1div2  10522  q0mod  10572  q1mod  10573  mulp1mod1  10582  m1modnnsub1  10587  modqm1p1mod0  10592  modqltm1p1mod  10593  bcval5  10980  swrd0g  11187  negfi  11734  xrmaxadd  11767  fprodle  12146  fprodmodd  12147  ege2le3  12177  sinltxirr  12267  p1modz1  12300  moddvds  12305  fsumdvds  12348  oddnn02np1  12386  oddge22np1  12387  evennn02n  12388  evennn2n  12389  bitsinv1lem  12467  3lcm2e6woprm  12603  6lcm4e12  12604  isprm6  12664  sqrt2irraplemnn  12696  fermltl  12751  phisum  12758  odzdvds  12763  reumodprminv  12771  pceu  12813  pcaddlem  12857  pcadd  12858  modxai  12934  modsubi  12937  ennnfonelemp1  12972  ennnfonelemkh  12978  ennnfonelemex  12980  exmidunben  12992  ssomct  13011  ssnnctlemct  13012  strslfv  13072  strleund  13131  prdsval  13301  prdsidlem  13475  pws0g  13479  idmhm  13497  mulgneg2  13688  gsumfzfsumlemm  14545  dvdsrzring  14561  expghmap  14565  zndvds  14607  cnbl0  15202  negfcncf  15274  cnrehmeocntop  15278  divcncfap  15282  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dvid  15363  dvidre  15365  dvmulxxbr  15370  dvexp  15379  plycjlemc  15428  plycj  15429  dvply1  15433  dvply2g  15434  sincn  15437  coscn  15438  coseq0q4123  15502  tangtx  15506  cosordlem  15517  wilthlem1  15648  1sgm2ppw  15663  perfectlem2  15668  lgslem1  15673  lgsvalmod  15692  lgsmod  15699  lgsdir2lem5  15705  lgsne0  15711  gausslemma2d  15742  lgseisenlem4  15746  lgseisen  15747  lgsquad2lem1  15754  lgsquad3  15757  2lgslem3a1  15770  2lgslem3b1  15771  2lgslem3c1  15772  2lgslem3d1  15773  pwf1oexmid  16324  nninfsellemdc  16335  trilpolemlt1  16368  apdiff  16375  iswomninnlem  16376