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  5059  relcoi2  5197  tfrlemi14d  6388  tfri1dALT  6406  mapsncnv  6751  findcard2d  6949  findcard2sd  6950  ac6sfi  6956  xpfi  6988  fifo  7041  updjudhcoinlf  7141  updjudhcoinrg  7142  updjud  7143  casefun  7146  omp1eomlem  7155  difinfsnlem  7160  djufun  7165  ctm  7170  ismkvnex  7216  cauappcvgprlemladd  7720  caucvgprprlemmu  7757  caucvgsrlemfv  7853  recidpirqlemcalc  7919  recidpirq  7920  axaddf  7930  axmulf  7931  xaddpnf1  9915  fldiv4lem1div2  10379  q0mod  10429  q1mod  10430  mulp1mod1  10439  m1modnnsub1  10444  modqm1p1mod0  10449  modqltm1p1mod  10450  bcval5  10837  negfi  11374  xrmaxadd  11407  fprodle  11786  fprodmodd  11787  ege2le3  11817  sinltxirr  11907  p1modz1  11940  moddvds  11945  oddnn02np1  12024  oddge22np1  12025  evennn02n  12026  evennn2n  12027  3lcm2e6woprm  12227  6lcm4e12  12228  isprm6  12288  sqrt2irraplemnn  12320  fermltl  12375  phisum  12381  odzdvds  12386  reumodprminv  12394  pceu  12436  pcaddlem  12480  pcadd  12481  ennnfonelemp1  12566  ennnfonelemkh  12572  ennnfonelemex  12574  exmidunben  12586  ssomct  12605  ssnnctlemct  12606  strslfv  12666  strleund  12724  idmhm  13044  mulgneg2  13229  gsumfzfsumlemm  14086  dvdsrzring  14102  expghmap  14106  zndvds  14148  cnbl0  14713  negfcncf  14785  cnrehmeocntop  14789  divcncfap  14793  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvid  14874  dvidre  14876  dvmulxxbr  14881  dvexp  14890  plycjlemc  14938  plycj  14939  dvply1  14943  sincn  14945  coscn  14946  coseq0q4123  15010  tangtx  15014  cosordlem  15025  wilthlem1  15153  lgslem1  15157  lgsvalmod  15176  lgsmod  15183  lgsdir2lem5  15189  lgsne0  15195  gausslemma2d  15226  lgseisenlem4  15230  lgseisen  15231  lgsquad2lem1  15238  lgsquad3  15241  2lgslem3a1  15254  2lgslem3b1  15255  2lgslem3c1  15256  2lgslem3d1  15257  pwf1oexmid  15560  nninfsellemdc  15570  trilpolemlt1  15601  apdiff  15608  iswomninnlem  15609