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  5127  relcoi2  5265  tfrlemi14d  6494  tfri1dALT  6512  mapsncnv  6859  findcard2d  7075  findcard2sd  7076  ac6sfi  7082  xpfi  7119  fifo  7173  updjudhcoinlf  7273  updjudhcoinrg  7274  updjud  7275  casefun  7278  omp1eomlem  7287  difinfsnlem  7292  djufun  7297  ctm  7302  ismkvnex  7348  cauappcvgprlemladd  7871  caucvgprprlemmu  7908  caucvgsrlemfv  8004  recidpirqlemcalc  8070  recidpirq  8071  axaddf  8081  axmulf  8082  xaddpnf1  10074  fldiv4lem1div2  10560  q0mod  10610  q1mod  10611  mulp1mod1  10620  m1modnnsub1  10625  modqm1p1mod0  10630  modqltm1p1mod  10631  bcval5  11018  swrd0g  11234  negfi  11782  xrmaxadd  11815  fprodle  12194  fprodmodd  12195  ege2le3  12225  sinltxirr  12315  p1modz1  12348  moddvds  12353  fsumdvds  12396  oddnn02np1  12434  oddge22np1  12435  evennn02n  12436  evennn2n  12437  bitsinv1lem  12515  3lcm2e6woprm  12651  6lcm4e12  12652  isprm6  12712  sqrt2irraplemnn  12744  fermltl  12799  phisum  12806  odzdvds  12811  reumodprminv  12819  pceu  12861  pcaddlem  12905  pcadd  12906  modxai  12982  modsubi  12985  ennnfonelemp1  13020  ennnfonelemkh  13026  ennnfonelemex  13028  exmidunben  13040  ssomct  13059  ssnnctlemct  13060  strslfv  13120  strleund  13179  prdsval  13349  prdsidlem  13523  pws0g  13527  idmhm  13545  mulgneg2  13736  gsumfzfsumlemm  14594  dvdsrzring  14610  expghmap  14614  zndvds  14656  cnbl0  15251  negfcncf  15323  cnrehmeocntop  15327  divcncfap  15331  dvidlemap  15408  dvidrelem  15409  dvidsslem  15410  dvid  15412  dvidre  15414  dvmulxxbr  15419  dvexp  15428  plycjlemc  15477  plycj  15478  dvply1  15482  dvply2g  15483  sincn  15486  coscn  15487  coseq0q4123  15551  tangtx  15555  cosordlem  15566  wilthlem1  15697  1sgm2ppw  15712  perfectlem2  15717  lgslem1  15722  lgsvalmod  15741  lgsmod  15748  lgsdir2lem5  15754  lgsne0  15760  gausslemma2d  15791  lgseisenlem4  15795  lgseisen  15796  lgsquad2lem1  15803  lgsquad3  15806  2lgslem3a1  15819  2lgslem3b1  15820  2lgslem3c1  15821  2lgslem3d1  15822  uspgr2wlkeq  16176  pwf1oexmid  16550  nninfsellemdc  16562  trilpolemlt1  16595  apdiff  16602  iswomninnlem  16603