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  5178  relcoi2  5316  supp0  6472  tfrlemi14d  6598  tfri1dALT  6616  mapsncnv  6971  findcard2d  7189  findcard2sd  7190  ac6sfi  7196  xpfi  7233  fifo  7308  updjudhcoinlf  7414  updjudhcoinrg  7415  updjud  7416  casefun  7419  omp1eomlem  7428  difinfsnlem  7433  djufun  7438  ctm  7443  ismkvnex  7489  cauappcvgprlemladd  8019  caucvgprprlemmu  8056  caucvgsrlemfv  8152  recidpirqlemcalc  8218  recidpirq  8219  axaddf  8229  axmulf  8230  xaddpnf1  10231  fldiv4lem1div2  10725  q0mod  10775  q1mod  10776  mulp1mod1  10785  m1modnnsub1  10790  modqm1p1mod0  10795  modqltm1p1mod  10796  bcval5  11184  hashmap  11251  swrd0g  11415  negfi  11977  xrmaxadd  12010  fprodle  12390  fprodmodd  12391  ege2le3  12421  sinltxirr  12511  p1modz1  12544  moddvds  12549  fsumdvds  12592  oddnn02np1  12630  oddge22np1  12631  evennn02n  12632  evennn2n  12633  bitsinv1lem  12711  3lcm2e6woprm  12847  6lcm4e12  12848  isprm6  12908  sqrt2irraplemnn  12940  fermltl  12995  phisum  13002  odzdvds  13007  reumodprminv  13015  pceu  13057  pcaddlem  13101  pcadd  13102  modxai  13178  modsubi  13181  ballotfilemofi  13202  ballotfilem2  13211  ballotfilemfmpn  13217  ballotfilem1ri  13261  ennnfonelemp1  13280  ennnfonelemkh  13286  ennnfonelemex  13288  exmidunben  13300  ssomct  13319  ssnnctlemct  13320  strslfv  13380  strleund  13440  idmhm  13759  mulgneg2  13942  gsumzfi  14141  prdsval  14156  prdsidlem  14176  pws0g  14196  dvdsrzring  14921  expghmap  14925  zndvds  14967  cnbl0  15618  negfcncf  15690  cnrehmeocntop  15694  divcncfap  15698  dvidlemap  15775  dvidrelem  15776  dvidsslem  15777  dvid  15779  dvidre  15781  dvmulxxbr  15786  dvexp  15795  plycjlemc  15844  plycj  15845  dvply1  15849  dvply2g  15850  sincn  15853  coscn  15854  coseq0q4123  15918  tangtx  15922  cosordlem  15933  log2tlbndlog2  16065  wilthlem1  16077  1sgm2ppw  16092  perfectlem2  16097  lgslem1  16102  lgsvalmod  16121  lgsmod  16128  lgsdir2lem5  16134  lgsne0  16140  gausslemma2d  16171  lgseisenlem4  16175  lgseisen  16176  lgsquad2lem1  16183  lgsquad3  16186  2lgslem3a1  16199  2lgslem3b1  16200  2lgslem3c1  16201  2lgslem3d1  16202  uspgr2wlkeq  16589  konigsberglem2  16713  pwf1oexmid  17012  nninfsellemdc  17027  trilpolemlt1  17064  apdiff  17071  qdiff  17072  iswomninnlem  17073