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  5022  relcoi2  5160  tfrlemi14d  6334  tfri1dALT  6352  mapsncnv  6695  findcard2d  6891  findcard2sd  6892  ac6sfi  6898  xpfi  6929  fifo  6979  updjudhcoinlf  7079  updjudhcoinrg  7080  updjud  7081  casefun  7084  omp1eomlem  7093  difinfsnlem  7098  djufun  7103  ctm  7108  ismkvnex  7153  cauappcvgprlemladd  7657  caucvgprprlemmu  7694  caucvgsrlemfv  7790  recidpirqlemcalc  7856  recidpirq  7857  axaddf  7867  axmulf  7868  xaddpnf1  9846  q0mod  10355  q1mod  10356  mulp1mod1  10365  m1modnnsub1  10370  modqm1p1mod0  10375  modqltm1p1mod  10376  bcval5  10743  negfi  11236  xrmaxadd  11269  fprodle  11648  fprodmodd  11649  ege2le3  11679  p1modz1  11801  moddvds  11806  oddnn02np1  11885  oddge22np1  11886  evennn02n  11887  evennn2n  11888  3lcm2e6woprm  12086  6lcm4e12  12087  isprm6  12147  sqrt2irraplemnn  12179  fermltl  12234  phisum  12240  odzdvds  12245  reumodprminv  12253  pceu  12295  pcaddlem  12338  pcadd  12339  ennnfonelemp1  12407  ennnfonelemkh  12413  ennnfonelemex  12415  exmidunben  12427  ssomct  12446  ssnnctlemct  12447  strslfv  12507  strleund  12562  idmhm  12860  mulgneg2  13017  dvdsrzring  13496  cnbl0  14037  negfcncf  14092  cnrehmeocntop  14096  dvidlemap  14163  dvid  14165  dvmulxxbr  14169  dvexp  14178  sincn  14193  coscn  14194  coseq0q4123  14258  tangtx  14262  cosordlem  14273  lgslem1  14404  lgsvalmod  14423  lgsmod  14430  lgsdir2lem5  14436  lgsne0  14442  pwf1oexmid  14752  nninfsellemdc  14762  trilpolemlt1  14792  apdiff  14799  iswomninnlem  14800