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  4926  relcoi2  5064  tfrlemi14d  6223  tfri1dALT  6241  mapsncnv  6582  findcard2d  6778  findcard2sd  6779  ac6sfi  6785  xpfi  6811  fifo  6861  updjudhcoinlf  6958  updjudhcoinrg  6959  updjud  6960  casefun  6963  omp1eomlem  6972  difinfsnlem  6977  djufun  6982  ctm  6987  ismkvnex  7022  cauappcvgprlemladd  7459  caucvgprprlemmu  7496  caucvgsrlemfv  7592  recidpirqlemcalc  7658  recidpirq  7659  axaddf  7669  axmulf  7670  xaddpnf1  9622  q0mod  10121  q1mod  10122  mulp1mod1  10131  m1modnnsub1  10136  modqm1p1mod0  10141  modqltm1p1mod  10142  bcval5  10502  negfi  10992  xrmaxadd  11023  ege2le3  11366  moddvds  11491  oddnn02np1  11566  oddge22np1  11567  evennn02n  11568  evennn2n  11569  3lcm2e6woprm  11756  6lcm4e12  11757  isprm6  11814  sqrt2irraplemnn  11846  ennnfonelemp1  11908  ennnfonelemkh  11914  ennnfonelemex  11916  exmidunben  11928  strslfv  11992  strleund  12036  cnbl0  12692  negfcncf  12747  cnrehmeocntop  12751  dvidlemap  12818  dvid  12820  dvmulxxbr  12824  dvexp  12833  sincn  12847  coscn  12848  coseq0q4123  12904  tangtx  12908  cosordlem  12919  pwf1oexmid  13183  nninfsellemdc  13195  trilpolemlt1  13223