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  5124  relcoi2  5262  tfrlemi14d  6490  tfri1dALT  6508  mapsncnv  6855  findcard2d  7066  findcard2sd  7067  ac6sfi  7073  xpfi  7110  fifo  7163  updjudhcoinlf  7263  updjudhcoinrg  7264  updjud  7265  casefun  7268  omp1eomlem  7277  difinfsnlem  7282  djufun  7287  ctm  7292  ismkvnex  7338  cauappcvgprlemladd  7861  caucvgprprlemmu  7898  caucvgsrlemfv  7994  recidpirqlemcalc  8060  recidpirq  8061  axaddf  8071  axmulf  8072  xaddpnf1  10059  fldiv4lem1div2  10544  q0mod  10594  q1mod  10595  mulp1mod1  10604  m1modnnsub1  10609  modqm1p1mod0  10614  modqltm1p1mod  10615  bcval5  11002  swrd0g  11213  negfi  11760  xrmaxadd  11793  fprodle  12172  fprodmodd  12173  ege2le3  12203  sinltxirr  12293  p1modz1  12326  moddvds  12331  fsumdvds  12374  oddnn02np1  12412  oddge22np1  12413  evennn02n  12414  evennn2n  12415  bitsinv1lem  12493  3lcm2e6woprm  12629  6lcm4e12  12630  isprm6  12690  sqrt2irraplemnn  12722  fermltl  12777  phisum  12784  odzdvds  12789  reumodprminv  12797  pceu  12839  pcaddlem  12883  pcadd  12884  modxai  12960  modsubi  12963  ennnfonelemp1  12998  ennnfonelemkh  13004  ennnfonelemex  13006  exmidunben  13018  ssomct  13037  ssnnctlemct  13038  strslfv  13098  strleund  13157  prdsval  13327  prdsidlem  13501  pws0g  13505  idmhm  13523  mulgneg2  13714  gsumfzfsumlemm  14572  dvdsrzring  14588  expghmap  14592  zndvds  14634  cnbl0  15229  negfcncf  15301  cnrehmeocntop  15305  divcncfap  15309  dvidlemap  15386  dvidrelem  15387  dvidsslem  15388  dvid  15390  dvidre  15392  dvmulxxbr  15397  dvexp  15406  plycjlemc  15455  plycj  15456  dvply1  15460  dvply2g  15461  sincn  15464  coscn  15465  coseq0q4123  15529  tangtx  15533  cosordlem  15544  wilthlem1  15675  1sgm2ppw  15690  perfectlem2  15695  lgslem1  15700  lgsvalmod  15719  lgsmod  15726  lgsdir2lem5  15732  lgsne0  15738  gausslemma2d  15769  lgseisenlem4  15773  lgseisen  15774  lgsquad2lem1  15781  lgsquad3  15784  2lgslem3a1  15797  2lgslem3b1  15798  2lgslem3c1  15799  2lgslem3d1  15800  uspgr2wlkeq  16137  pwf1oexmid  16478  nninfsellemdc  16490  trilpolemlt1  16523  apdiff  16530  iswomninnlem  16531