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  5003  relcoi2  5141  tfrlemi14d  6312  tfri1dALT  6330  mapsncnv  6673  findcard2d  6869  findcard2sd  6870  ac6sfi  6876  xpfi  6907  fifo  6957  updjudhcoinlf  7057  updjudhcoinrg  7058  updjud  7059  casefun  7062  omp1eomlem  7071  difinfsnlem  7076  djufun  7081  ctm  7086  ismkvnex  7131  cauappcvgprlemladd  7620  caucvgprprlemmu  7657  caucvgsrlemfv  7753  recidpirqlemcalc  7819  recidpirq  7820  axaddf  7830  axmulf  7831  xaddpnf1  9803  q0mod  10311  q1mod  10312  mulp1mod1  10321  m1modnnsub1  10326  modqm1p1mod0  10331  modqltm1p1mod  10332  bcval5  10697  negfi  11191  xrmaxadd  11224  fprodle  11603  fprodmodd  11604  ege2le3  11634  p1modz1  11756  moddvds  11761  oddnn02np1  11839  oddge22np1  11840  evennn02n  11841  evennn2n  11842  3lcm2e6woprm  12040  6lcm4e12  12041  isprm6  12101  sqrt2irraplemnn  12133  fermltl  12188  phisum  12194  odzdvds  12199  reumodprminv  12207  pceu  12249  pcaddlem  12292  pcadd  12293  ennnfonelemp1  12361  ennnfonelemkh  12367  ennnfonelemex  12369  exmidunben  12381  ssomct  12400  ssnnctlemct  12401  strslfv  12460  strleund  12506  idmhm  12692  cnbl0  13328  negfcncf  13383  cnrehmeocntop  13387  dvidlemap  13454  dvid  13456  dvmulxxbr  13460  dvexp  13469  sincn  13484  coscn  13485  coseq0q4123  13549  tangtx  13553  cosordlem  13564  lgslem1  13695  lgsvalmod  13714  lgsmod  13721  lgsdir2lem5  13727  lgsne0  13733  pwf1oexmid  14032  nninfsellemdc  14043  trilpolemlt1  14073  apdiff  14080  iswomninnlem  14081