Theorem mp1i 10

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

Hypotheses

Ref	Expression
mp1i.a	⊢ 𝜑
mp1i.b	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
mp1i	⊢ (𝜒 → 𝜓)

Proof of Theorem mp1i

Step	Hyp	Ref	Expression
1		mp1i.a	. . 3 ⊢ 𝜑
2		mp1i.b	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	ax-mp 5	. 2 ⊢ 𝜓
4	3	a1i 9	1 ⊢ (𝜒 → 𝜓)

Syntax hints:   → wi 4

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

This theorem is referenced by:  poirr2  4939  relcoi2  5077  tfrlemi14d  6238  tfri1dALT  6256  mapsncnv  6597  findcard2d  6793  findcard2sd  6794  ac6sfi  6800  xpfi  6826  fifo  6876  updjudhcoinlf  6973  updjudhcoinrg  6974  updjud  6975  casefun  6978  omp1eomlem  6987  difinfsnlem  6992  djufun  6997  ctm  7002  ismkvnex  7037  cauappcvgprlemladd  7490  caucvgprprlemmu  7527  caucvgsrlemfv  7623  recidpirqlemcalc  7689  recidpirq  7690  axaddf  7700  axmulf  7701  xaddpnf1  9659  q0mod  10159  q1mod  10160  mulp1mod1  10169  m1modnnsub1  10174  modqm1p1mod0  10179  modqltm1p1mod  10180  bcval5  10541  negfi  11031  xrmaxadd  11062  ege2le3  11414  moddvds  11538  oddnn02np1  11613  oddge22np1  11614  evennn02n  11615  evennn2n  11616  3lcm2e6woprm  11803  6lcm4e12  11804  isprm6  11861  sqrt2irraplemnn  11893  ennnfonelemp1  11955  ennnfonelemkh  11961  ennnfonelemex  11963  exmidunben  11975  strslfv  12042  strleund  12086  cnbl0  12742  negfcncf  12797  cnrehmeocntop  12801  dvidlemap  12868  dvid  12870  dvmulxxbr  12874  dvexp  12883  sincn  12898  coscn  12899  coseq0q4123  12963  tangtx  12967  cosordlem  12978  pwf1oexmid  13367  nninfsellemdc  13381  trilpolemlt1  13409  apdiff  13416  iswomninnlem  13417