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  5097  relcoi2  5235  tfrlemi14d  6449  tfri1dALT  6467  mapsncnv  6812  findcard2d  7021  findcard2sd  7022  ac6sfi  7028  xpfi  7062  fifo  7115  updjudhcoinlf  7215  updjudhcoinrg  7216  updjud  7217  casefun  7220  omp1eomlem  7229  difinfsnlem  7234  djufun  7239  ctm  7244  ismkvnex  7290  cauappcvgprlemladd  7813  caucvgprprlemmu  7850  caucvgsrlemfv  7946  recidpirqlemcalc  8012  recidpirq  8013  axaddf  8023  axmulf  8024  xaddpnf1  10010  fldiv4lem1div2  10494  q0mod  10544  q1mod  10545  mulp1mod1  10554  m1modnnsub1  10559  modqm1p1mod0  10564  modqltm1p1mod  10565  bcval5  10952  swrd0g  11158  negfi  11705  xrmaxadd  11738  fprodle  12117  fprodmodd  12118  ege2le3  12148  sinltxirr  12238  p1modz1  12271  moddvds  12276  fsumdvds  12319  oddnn02np1  12357  oddge22np1  12358  evennn02n  12359  evennn2n  12360  bitsinv1lem  12438  3lcm2e6woprm  12574  6lcm4e12  12575  isprm6  12635  sqrt2irraplemnn  12667  fermltl  12722  phisum  12729  odzdvds  12734  reumodprminv  12742  pceu  12784  pcaddlem  12828  pcadd  12829  modxai  12905  modsubi  12908  ennnfonelemp1  12943  ennnfonelemkh  12949  ennnfonelemex  12951  exmidunben  12963  ssomct  12982  ssnnctlemct  12983  strslfv  13043  strleund  13102  prdsval  13272  prdsidlem  13446  pws0g  13450  idmhm  13468  mulgneg2  13659  gsumfzfsumlemm  14516  dvdsrzring  14532  expghmap  14536  zndvds  14578  cnbl0  15173  negfcncf  15245  cnrehmeocntop  15249  divcncfap  15253  dvidlemap  15330  dvidrelem  15331  dvidsslem  15332  dvid  15334  dvidre  15336  dvmulxxbr  15341  dvexp  15350  plycjlemc  15399  plycj  15400  dvply1  15404  dvply2g  15405  sincn  15408  coscn  15409  coseq0q4123  15473  tangtx  15477  cosordlem  15488  wilthlem1  15619  1sgm2ppw  15634  perfectlem2  15639  lgslem1  15644  lgsvalmod  15663  lgsmod  15670  lgsdir2lem5  15676  lgsne0  15682  gausslemma2d  15713  lgseisenlem4  15717  lgseisen  15718  lgsquad2lem1  15725  lgsquad3  15728  2lgslem3a1  15741  2lgslem3b1  15742  2lgslem3c1  15743  2lgslem3d1  15744  pwf1oexmid  16276  nninfsellemdc  16287  trilpolemlt1  16320  apdiff  16327  iswomninnlem  16328