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 ⊢ (𝜒 → 𝜓)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6

This theorem is used by:  poirr2  5180  relcoi2  5318  supp0  6478  tfrlemi14d  6604  tfri1dALT  6622  mapsncnv  6977  findcard2d  7195  findcard2sd  7196  ac6sfi  7202  xpfi  7239  fifo  7314  updjudhcoinlf  7420  updjudhcoinrg  7421  updjud  7422  casefun  7425  omp1eomlem  7434  difinfsnlem  7439  djufun  7444  ctm  7449  ismkvnex  7495  cauappcvgprlemladd  8025  caucvgprprlemmu  8062  caucvgsrlemfv  8158  recidpirqlemcalc  8224  recidpirq  8225  axaddf  8235  axmulf  8236  xaddpnf1  10250  fldiv4lem1div2  10744  q0mod  10794  q1mod  10795  mulp1mod1  10804  m1modnnsub1  10809  modqm1p1mod0  10814  modqltm1p1mod  10815  bcval5  11203  hashmap  11270  swrd0g  11434  negfi  11996  xrmaxadd  12029  fprodle  12409  fprodmodd  12410  ege2le3  12440  sinltxirr  12530  p1modz1  12563  moddvds  12568  fsumdvds  12611  oddnn02np1  12649  oddge22np1  12650  evennn02n  12651  evennn2n  12652  bitsinv1lem  12730  3lcm2e6woprm  12866  6lcm4e12  12867  isprm6  12927  sqrt2irraplemnn  12959  fermltl  13014  phisum  13021  odzdvds  13026  reumodprminv  13034  pceu  13076  pcaddlem  13120  pcadd  13121  modxai  13197  modsubi  13200  ballotfilemofi  13221  ballotfilem2  13230  ballotfilemfmpn  13236  ballotfilem1ri  13280  ennnfonelemp1  13299  ennnfonelemkh  13305  ennnfonelemex  13307  exmidunben  13319  ssomct  13338  ssnnctlemct  13339  strslfv  13399  strleund  13459  idmhm  13778  mulgneg2  13961  gsumzfi  14160  prdsval  14175  prdsidlem  14195  pws0g  14215  dvdsrzring  14940  expghmap  14944  zndvds  14986  cnbl0  15637  negfcncf  15709  cnrehmeocntop  15713  divcncfap  15717  dvidlemap  15794  dvidrelem  15795  dvidsslem  15796  dvid  15798  dvidre  15800  dvmulxxbr  15805  dvexp  15814  plycjlemc  15863  plycj  15864  dvply1  15868  dvply2g  15869  sincn  15872  coscn  15873  coseq0q4123  15938  tangtx  15942  cosordlem  15953  log2tlbndlog2  16088  wilthlem1  16100  1sgm2ppw  16115  perfectlem2  16120  lgslem1  16131  lgsvalmod  16150  lgsmod  16157  lgsdir2lem5  16163  lgsne0  16169  gausslemma2d  16200  lgseisenlem4  16204  lgseisen  16205  lgsquad2lem1  16212  lgsquad3  16215  2lgslem3a1  16228  2lgslem3b1  16229  2lgslem3c1  16230  2lgslem3d1  16231  uspgr2wlkeq  16618  konigsberglem2  16742  pwf1oexmid  17041  nninfsellemdc  17065  trilpolemlt1  17102  apdiff  17109  qdiff  17110  iswomninnlem  17111