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  10258  fldiv4lem1div2  10755  q0mod  10805  q1mod  10806  mulp1mod1  10815  m1modnnsub1  10820  modqm1p1mod0  10825  modqltm1p1mod  10826  bcval5  11215  hashmap  11282  swrd0g  11446  negfi  12009  xrmaxadd  12043  fprodle  12423  fprodmodd  12424  ege2le3  12454  sinltxirr  12544  p1modz1  12577  moddvds  12582  fsumdvds  12625  oddnn02np1  12663  oddge22np1  12664  evennn02n  12665  evennn2n  12666  bitsinv1lem  12744  3lcm2e6woprm  12880  6lcm4e12  12881  isprm6  12942  sqrt2irraplemnn  12975  nn0sqdcq  13004  fermltl  13032  phisum  13039  odzdvds  13044  reumodprminv  13052  pceu  13094  pcaddlem  13138  pcadd  13139  modxai  13215  modsubi  13219  prmlem0  13240  ballotfilemofi  13268  ballotfilem2  13277  ballotfilemfmpn  13283  ballotfilem1ri  13327  ennnfonelemp1  13346  ennnfonelemkh  13352  ennnfonelemex  13354  exmidunben  13366  ssomct  13385  ssnnctlemct  13386  strslfv  13446  strleund  13506  idmhm  13825  mulgneg2  14008  gsumzfi  14207  prdsval  14222  prdsidlem  14242  pws0g  14262  dvdsrzring  14987  expghmap  14991  zndvds  15033  cnbl0  15684  negfcncf  15756  cnrehmeocntop  15760  divcncfap  15764  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvid  15845  dvidre  15847  dvmulxxbr  15852  dvexp  15861  plycjlemc  15910  plycj  15911  dvply1  15915  dvply2g  15916  sincn  15919  coscn  15920  coseq0q4123  15985  tangtx  15989  cosordlem  16000  log2tlbndlog2  16139  wilthlem1  16151  chtqrpcl  16198  1sgm2ppw  16208  perfectlem2  16219  lgslem1  16238  lgsvalmod  16257  lgsmod  16264  lgsdir2lem5  16270  lgsne0  16276  gausslemma2d  16307  lgseisenlem4  16311  lgseisen  16312  lgsquad2lem1  16319  lgsquad3  16322  2lgslem3a1  16335  2lgslem3b1  16336  2lgslem3c1  16337  2lgslem3d1  16338  uspgr2wlkeq  16725  konigsberglem2  16849  pwf1oexmid  17148  nninfsellemdc  17172  trilpolemlt1  17209  apdiff  17216  qdiff  17217  iswomninnlem  17218