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  5183  relcoi2  5321  supp0  6482  tfrlemi14d  6608  tfri1dALT  6626  mapsncnv  6982  findcard2d  7200  findcard2sd  7201  ac6sfi  7207  xpfi  7244  fifo  7320  updjudhcoinlf  7427  updjudhcoinrg  7428  updjud  7429  casefun  7432  omp1eomlem  7441  difinfsnlem  7446  djufun  7451  ctm  7456  ismkvnex  7502  cauappcvgprlemladd  8032  caucvgprprlemmu  8069  caucvgsrlemfv  8165  recidpirqlemcalc  8231  recidpirq  8232  axaddf  8242  axmulf  8243  xaddpnf1  10266  fldiv4lem1div2  10764  q0mod  10814  q1mod  10815  mulp1mod1  10824  m1modnnsub1  10829  modqm1p1mod0  10834  modqltm1p1mod  10835  bcval5  11224  hashmap  11291  swrd0g  11455  negfi  12018  xrmaxadd  12053  fprodle  12433  fprodmodd  12434  ege2le3  12464  sinltxirr  12554  p1modz1  12587  moddvds  12592  fsumdvds  12635  oddnn02np1  12673  oddge22np1  12674  evennn02n  12675  evennn2n  12676  bitsinv1lem  12754  3lcm2e6woprm  12890  6lcm4e12  12891  isprm6  12952  sqrt2irraplemnn  12985  nn0sqdcq  13014  fermltl  13042  phisum  13049  odzdvds  13054  reumodprminv  13062  pceu  13104  pcaddlem  13148  pcadd  13149  modxai  13225  modsubi  13229  prmlem0  13250  ballotfilemofi  13278  ballotfilem2  13287  ballotfilemfmpn  13293  ballotfilem1ri  13337  ennnfonelemp1  13356  ennnfonelemkh  13362  ennnfonelemex  13364  exmidunben  13376  ssomct  13395  ssnnctlemct  13396  strslfv  13456  strleund  13517  idmhm  13836  mulgneg2  14019  gsumzfi  14249  gsum2dfilem2  14273  prdsval  14281  prdsidlem  14301  pws0g  14321  dvdsrzring  15048  expghmap  15052  zndvds  15094  psrlidmfi  15204  cnbl0  15772  negfcncf  15844  cnrehmeocntop  15848  divcncfap  15852  dvidlemap  15929  dvidrelem  15930  dvidsslem  15931  dvid  15933  dvidre  15935  dvmulxxbr  15940  dvexp  15949  plycjlemc  15998  plycj  15999  dvply1  16003  dvply2g  16004  sincn  16007  coscn  16008  coseq0q4123  16073  tangtx  16077  cosordlem  16089  log2tlbndlog2  16232  wilthlem1  16244  chtqrpcl  16291  1sgm2ppw  16301  perfectlem2  16312  bposlem7  16329  lgslem1  16336  lgsvalmod  16355  lgsmod  16362  lgsdir2lem5  16368  lgsne0  16374  gausslemma2d  16405  lgseisenlem4  16409  lgseisen  16410  lgsquad2lem1  16417  lgsquad3  16420  2lgslem3a1  16433  2lgslem3b1  16434  2lgslem3c1  16435  2lgslem3d1  16436  uspgr2wlkeq  16823  konigsberglem2  16947  pwf1oexmid  17246  nninfsellemdc  17271  trilpolemlt1  17309  apdiff  17316  qdiff  17317  iswomninnlem  17318