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  5121  relcoi2  5259  tfrlemi14d  6485  tfri1dALT  6503  mapsncnv  6850  findcard2d  7061  findcard2sd  7062  ac6sfi  7068  xpfi  7102  fifo  7155  updjudhcoinlf  7255  updjudhcoinrg  7256  updjud  7257  casefun  7260  omp1eomlem  7269  difinfsnlem  7274  djufun  7279  ctm  7284  ismkvnex  7330  cauappcvgprlemladd  7853  caucvgprprlemmu  7890  caucvgsrlemfv  7986  recidpirqlemcalc  8052  recidpirq  8053  axaddf  8063  axmulf  8064  xaddpnf1  10050  fldiv4lem1div2  10535  q0mod  10585  q1mod  10586  mulp1mod1  10595  m1modnnsub1  10600  modqm1p1mod0  10605  modqltm1p1mod  10606  bcval5  10993  swrd0g  11200  negfi  11747  xrmaxadd  11780  fprodle  12159  fprodmodd  12160  ege2le3  12190  sinltxirr  12280  p1modz1  12313  moddvds  12318  fsumdvds  12361  oddnn02np1  12399  oddge22np1  12400  evennn02n  12401  evennn2n  12402  bitsinv1lem  12480  3lcm2e6woprm  12616  6lcm4e12  12617  isprm6  12677  sqrt2irraplemnn  12709  fermltl  12764  phisum  12771  odzdvds  12776  reumodprminv  12784  pceu  12826  pcaddlem  12870  pcadd  12871  modxai  12947  modsubi  12950  ennnfonelemp1  12985  ennnfonelemkh  12991  ennnfonelemex  12993  exmidunben  13005  ssomct  13024  ssnnctlemct  13025  strslfv  13085  strleund  13144  prdsval  13314  prdsidlem  13488  pws0g  13492  idmhm  13510  mulgneg2  13701  gsumfzfsumlemm  14559  dvdsrzring  14575  expghmap  14579  zndvds  14621  cnbl0  15216  negfcncf  15288  cnrehmeocntop  15292  divcncfap  15296  dvidlemap  15373  dvidrelem  15374  dvidsslem  15375  dvid  15377  dvidre  15379  dvmulxxbr  15384  dvexp  15393  plycjlemc  15442  plycj  15443  dvply1  15447  dvply2g  15448  sincn  15451  coscn  15452  coseq0q4123  15516  tangtx  15520  cosordlem  15531  wilthlem1  15662  1sgm2ppw  15677  perfectlem2  15682  lgslem1  15687  lgsvalmod  15706  lgsmod  15713  lgsdir2lem5  15719  lgsne0  15725  gausslemma2d  15756  lgseisenlem4  15760  lgseisen  15761  lgsquad2lem1  15768  lgsquad3  15771  2lgslem3a1  15784  2lgslem3b1  15785  2lgslem3c1  15786  2lgslem3d1  15787  uspgr2wlkeq  16086  pwf1oexmid  16394  nninfsellemdc  16406  trilpolemlt1  16439  apdiff  16446  iswomninnlem  16447