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  5033  relcoi2  5171  tfrlemi14d  6348  tfri1dALT  6366  mapsncnv  6709  findcard2d  6905  findcard2sd  6906  ac6sfi  6912  xpfi  6943  fifo  6993  updjudhcoinlf  7093  updjudhcoinrg  7094  updjud  7095  casefun  7098  omp1eomlem  7107  difinfsnlem  7112  djufun  7117  ctm  7122  ismkvnex  7167  cauappcvgprlemladd  7671  caucvgprprlemmu  7708  caucvgsrlemfv  7804  recidpirqlemcalc  7870  recidpirq  7871  axaddf  7881  axmulf  7882  xaddpnf1  9860  q0mod  10369  q1mod  10370  mulp1mod1  10379  m1modnnsub1  10384  modqm1p1mod0  10389  modqltm1p1mod  10390  bcval5  10757  negfi  11250  xrmaxadd  11283  fprodle  11662  fprodmodd  11663  ege2le3  11693  p1modz1  11815  moddvds  11820  oddnn02np1  11899  oddge22np1  11900  evennn02n  11901  evennn2n  11902  3lcm2e6woprm  12100  6lcm4e12  12101  isprm6  12161  sqrt2irraplemnn  12193  fermltl  12248  phisum  12254  odzdvds  12259  reumodprminv  12267  pceu  12309  pcaddlem  12352  pcadd  12353  ennnfonelemp1  12421  ennnfonelemkh  12427  ennnfonelemex  12429  exmidunben  12441  ssomct  12460  ssnnctlemct  12461  strslfv  12521  strleund  12577  idmhm  12882  mulgneg2  13049  dvdsrzring  13775  cnbl0  14330  negfcncf  14385  cnrehmeocntop  14389  dvidlemap  14456  dvid  14458  dvmulxxbr  14462  dvexp  14471  sincn  14486  coscn  14487  coseq0q4123  14551  tangtx  14555  cosordlem  14566  lgslem1  14697  lgsvalmod  14716  lgsmod  14723  lgsdir2lem5  14729  lgsne0  14735  pwf1oexmid  15046  nninfsellemdc  15056  trilpolemlt1  15086  apdiff  15093  iswomninnlem  15094