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  5125  relcoi2  5263  tfrlemi14d  6492  tfri1dALT  6510  mapsncnv  6857  findcard2d  7071  findcard2sd  7072  ac6sfi  7078  xpfi  7115  fifo  7168  updjudhcoinlf  7268  updjudhcoinrg  7269  updjud  7270  casefun  7273  omp1eomlem  7282  difinfsnlem  7287  djufun  7292  ctm  7297  ismkvnex  7343  cauappcvgprlemladd  7866  caucvgprprlemmu  7903  caucvgsrlemfv  7999  recidpirqlemcalc  8065  recidpirq  8066  axaddf  8076  axmulf  8077  xaddpnf1  10069  fldiv4lem1div2  10555  q0mod  10605  q1mod  10606  mulp1mod1  10615  m1modnnsub1  10620  modqm1p1mod0  10625  modqltm1p1mod  10626  bcval5  11013  swrd0g  11228  negfi  11776  xrmaxadd  11809  fprodle  12188  fprodmodd  12189  ege2le3  12219  sinltxirr  12309  p1modz1  12342  moddvds  12347  fsumdvds  12390  oddnn02np1  12428  oddge22np1  12429  evennn02n  12430  evennn2n  12431  bitsinv1lem  12509  3lcm2e6woprm  12645  6lcm4e12  12646  isprm6  12706  sqrt2irraplemnn  12738  fermltl  12793  phisum  12800  odzdvds  12805  reumodprminv  12813  pceu  12855  pcaddlem  12899  pcadd  12900  modxai  12976  modsubi  12979  ennnfonelemp1  13014  ennnfonelemkh  13020  ennnfonelemex  13022  exmidunben  13034  ssomct  13053  ssnnctlemct  13054  strslfv  13114  strleund  13173  prdsval  13343  prdsidlem  13517  pws0g  13521  idmhm  13539  mulgneg2  13730  gsumfzfsumlemm  14588  dvdsrzring  14604  expghmap  14608  zndvds  14650  cnbl0  15245  negfcncf  15317  cnrehmeocntop  15321  divcncfap  15325  dvidlemap  15402  dvidrelem  15403  dvidsslem  15404  dvid  15406  dvidre  15408  dvmulxxbr  15413  dvexp  15422  plycjlemc  15471  plycj  15472  dvply1  15476  dvply2g  15477  sincn  15480  coscn  15481  coseq0q4123  15545  tangtx  15549  cosordlem  15560  wilthlem1  15691  1sgm2ppw  15706  perfectlem2  15711  lgslem1  15716  lgsvalmod  15735  lgsmod  15742  lgsdir2lem5  15748  lgsne0  15754  gausslemma2d  15785  lgseisenlem4  15789  lgseisen  15790  lgsquad2lem1  15797  lgsquad3  15800  2lgslem3a1  15813  2lgslem3b1  15814  2lgslem3c1  15815  2lgslem3d1  15816  uspgr2wlkeq  16153  pwf1oexmid  16510  nninfsellemdc  16522  trilpolemlt1  16555  apdiff  16562  iswomninnlem  16563