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  5160  relcoi2  5298  supp0  6451  tfrlemi14d  6577  tfri1dALT  6595  mapsncnv  6943  findcard2d  7161  findcard2sd  7162  ac6sfi  7168  xpfi  7205  fifo  7280  updjudhcoinlf  7384  updjudhcoinrg  7385  updjud  7386  casefun  7389  omp1eomlem  7398  difinfsnlem  7403  djufun  7408  ctm  7413  ismkvnex  7459  cauappcvgprlemladd  7989  caucvgprprlemmu  8026  caucvgsrlemfv  8122  recidpirqlemcalc  8188  recidpirq  8189  axaddf  8199  axmulf  8200  xaddpnf1  10201  fldiv4lem1div2  10694  q0mod  10744  q1mod  10745  mulp1mod1  10754  m1modnnsub1  10759  modqm1p1mod0  10764  modqltm1p1mod  10765  bcval5  11153  hashmap  11220  swrd0g  11380  negfi  11941  xrmaxadd  11974  fprodle  12354  fprodmodd  12355  ege2le3  12385  sinltxirr  12475  p1modz1  12508  moddvds  12513  fsumdvds  12556  oddnn02np1  12594  oddge22np1  12595  evennn02n  12596  evennn2n  12597  bitsinv1lem  12675  3lcm2e6woprm  12811  6lcm4e12  12812  isprm6  12872  sqrt2irraplemnn  12904  fermltl  12959  phisum  12966  odzdvds  12971  reumodprminv  12979  pceu  13021  pcaddlem  13065  pcadd  13066  modxai  13142  modsubi  13145  ballotfilemofi  13166  ballotfilem2  13175  ballotfilemfmpn  13181  ballotfilem1ri  13225  ennnfonelemp1  13244  ennnfonelemkh  13250  ennnfonelemex  13252  exmidunben  13264  ssomct  13283  ssnnctlemct  13284  strslfv  13344  strleund  13403  idmhm  13727  mulgneg2  13912  gfsumz  14112  prdsval  14118  prdsidlem  14138  pws0g  14158  gsumfzfsumlemm  14864  dvdsrzring  14880  expghmap  14884  zndvds  14926  cnbl0  15528  negfcncf  15600  cnrehmeocntop  15604  divcncfap  15608  dvidlemap  15685  dvidrelem  15686  dvidsslem  15687  dvid  15689  dvidre  15691  dvmulxxbr  15696  dvexp  15705  plycjlemc  15754  plycj  15755  dvply1  15759  dvply2g  15760  sincn  15763  coscn  15764  coseq0q4123  15828  tangtx  15832  cosordlem  15843  wilthlem1  15977  1sgm2ppw  15992  perfectlem2  15997  lgslem1  16002  lgsvalmod  16021  lgsmod  16028  lgsdir2lem5  16034  lgsne0  16040  gausslemma2d  16071  lgseisenlem4  16075  lgseisen  16076  lgsquad2lem1  16083  lgsquad3  16086  2lgslem3a1  16099  2lgslem3b1  16100  2lgslem3c1  16101  2lgslem3d1  16102  uspgr2wlkeq  16489  konigsberglem2  16613  pwf1oexmid  16912  nninfsellemdc  16927  trilpolemlt1  16964  apdiff  16971  qdiff  16972  iswomninnlem  16973