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  5021  relcoi2  5159  tfrlemi14d  6333  tfri1dALT  6351  mapsncnv  6694  findcard2d  6890  findcard2sd  6891  ac6sfi  6897  xpfi  6928  fifo  6978  updjudhcoinlf  7078  updjudhcoinrg  7079  updjud  7080  casefun  7083  omp1eomlem  7092  difinfsnlem  7097  djufun  7102  ctm  7107  ismkvnex  7152  cauappcvgprlemladd  7656  caucvgprprlemmu  7693  caucvgsrlemfv  7789  recidpirqlemcalc  7855  recidpirq  7856  axaddf  7866  axmulf  7867  xaddpnf1  9844  q0mod  10352  q1mod  10353  mulp1mod1  10362  m1modnnsub1  10367  modqm1p1mod0  10372  modqltm1p1mod  10373  bcval5  10738  negfi  11231  xrmaxadd  11264  fprodle  11643  fprodmodd  11644  ege2le3  11674  p1modz1  11796  moddvds  11801  oddnn02np1  11879  oddge22np1  11880  evennn02n  11881  evennn2n  11882  3lcm2e6woprm  12080  6lcm4e12  12081  isprm6  12141  sqrt2irraplemnn  12173  fermltl  12228  phisum  12234  odzdvds  12239  reumodprminv  12247  pceu  12289  pcaddlem  12332  pcadd  12333  ennnfonelemp1  12401  ennnfonelemkh  12407  ennnfonelemex  12409  exmidunben  12421  ssomct  12440  ssnnctlemct  12441  strslfv  12501  strleund  12556  idmhm  12854  mulgneg2  13010  dvdsrzring  13424  cnbl0  13965  negfcncf  14020  cnrehmeocntop  14024  dvidlemap  14091  dvid  14093  dvmulxxbr  14097  dvexp  14106  sincn  14121  coscn  14122  coseq0q4123  14186  tangtx  14190  cosordlem  14201  lgslem1  14332  lgsvalmod  14351  lgsmod  14358  lgsdir2lem5  14364  lgsne0  14370  pwf1oexmid  14669  nninfsellemdc  14679  trilpolemlt1  14709  apdiff  14716  iswomninnlem  14717