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  5063  relcoi2  5201  tfrlemi14d  6400  tfri1dALT  6418  mapsncnv  6763  findcard2d  6961  findcard2sd  6962  ac6sfi  6968  xpfi  7002  fifo  7055  updjudhcoinlf  7155  updjudhcoinrg  7156  updjud  7157  casefun  7160  omp1eomlem  7169  difinfsnlem  7174  djufun  7179  ctm  7184  ismkvnex  7230  cauappcvgprlemladd  7744  caucvgprprlemmu  7781  caucvgsrlemfv  7877  recidpirqlemcalc  7943  recidpirq  7944  axaddf  7954  axmulf  7955  xaddpnf1  9940  fldiv4lem1div2  10416  q0mod  10466  q1mod  10467  mulp1mod1  10476  m1modnnsub1  10481  modqm1p1mod0  10486  modqltm1p1mod  10487  bcval5  10874  negfi  11412  xrmaxadd  11445  fprodle  11824  fprodmodd  11825  ege2le3  11855  sinltxirr  11945  p1modz1  11978  moddvds  11983  fsumdvds  12026  oddnn02np1  12064  oddge22np1  12065  evennn02n  12066  evennn2n  12067  bitsinv1lem  12145  3lcm2e6woprm  12281  6lcm4e12  12282  isprm6  12342  sqrt2irraplemnn  12374  fermltl  12429  phisum  12436  odzdvds  12441  reumodprminv  12449  pceu  12491  pcaddlem  12535  pcadd  12536  modxai  12612  modsubi  12615  ennnfonelemp1  12650  ennnfonelemkh  12656  ennnfonelemex  12658  exmidunben  12670  ssomct  12689  ssnnctlemct  12690  strslfv  12750  strleund  12808  prdsval  12977  prdsidlem  13151  pws0g  13155  idmhm  13173  mulgneg2  13364  gsumfzfsumlemm  14221  dvdsrzring  14237  expghmap  14241  zndvds  14283  cnbl0  14878  negfcncf  14950  cnrehmeocntop  14954  divcncfap  14958  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvid  15039  dvidre  15041  dvmulxxbr  15046  dvexp  15055  plycjlemc  15104  plycj  15105  dvply1  15109  dvply2g  15110  sincn  15113  coscn  15114  coseq0q4123  15178  tangtx  15182  cosordlem  15193  wilthlem1  15324  1sgm2ppw  15339  perfectlem2  15344  lgslem1  15349  lgsvalmod  15368  lgsmod  15375  lgsdir2lem5  15381  lgsne0  15387  gausslemma2d  15418  lgseisenlem4  15422  lgseisen  15423  lgsquad2lem1  15430  lgsquad3  15433  2lgslem3a1  15446  2lgslem3b1  15447  2lgslem3c1  15448  2lgslem3d1  15449  pwf1oexmid  15754  nninfsellemdc  15765  trilpolemlt1  15798  apdiff  15805  iswomninnlem  15806