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  5080  relcoi2  5218  tfrlemi14d  6426  tfri1dALT  6444  mapsncnv  6789  findcard2d  6995  findcard2sd  6996  ac6sfi  7002  xpfi  7036  fifo  7089  updjudhcoinlf  7189  updjudhcoinrg  7190  updjud  7191  casefun  7194  omp1eomlem  7203  difinfsnlem  7208  djufun  7213  ctm  7218  ismkvnex  7264  cauappcvgprlemladd  7778  caucvgprprlemmu  7815  caucvgsrlemfv  7911  recidpirqlemcalc  7977  recidpirq  7978  axaddf  7988  axmulf  7989  xaddpnf1  9975  fldiv4lem1div2  10457  q0mod  10507  q1mod  10508  mulp1mod1  10517  m1modnnsub1  10522  modqm1p1mod0  10527  modqltm1p1mod  10528  bcval5  10915  swrd0g  11121  negfi  11583  xrmaxadd  11616  fprodle  11995  fprodmodd  11996  ege2le3  12026  sinltxirr  12116  p1modz1  12149  moddvds  12154  fsumdvds  12197  oddnn02np1  12235  oddge22np1  12236  evennn02n  12237  evennn2n  12238  bitsinv1lem  12316  3lcm2e6woprm  12452  6lcm4e12  12453  isprm6  12513  sqrt2irraplemnn  12545  fermltl  12600  phisum  12607  odzdvds  12612  reumodprminv  12620  pceu  12662  pcaddlem  12706  pcadd  12707  modxai  12783  modsubi  12786  ennnfonelemp1  12821  ennnfonelemkh  12827  ennnfonelemex  12829  exmidunben  12841  ssomct  12860  ssnnctlemct  12861  strslfv  12921  strleund  12979  prdsval  13149  prdsidlem  13323  pws0g  13327  idmhm  13345  mulgneg2  13536  gsumfzfsumlemm  14393  dvdsrzring  14409  expghmap  14413  zndvds  14455  cnbl0  15050  negfcncf  15122  cnrehmeocntop  15126  divcncfap  15130  dvidlemap  15207  dvidrelem  15208  dvidsslem  15209  dvid  15211  dvidre  15213  dvmulxxbr  15218  dvexp  15227  plycjlemc  15276  plycj  15277  dvply1  15281  dvply2g  15282  sincn  15285  coscn  15286  coseq0q4123  15350  tangtx  15354  cosordlem  15365  wilthlem1  15496  1sgm2ppw  15511  perfectlem2  15516  lgslem1  15521  lgsvalmod  15540  lgsmod  15547  lgsdir2lem5  15553  lgsne0  15559  gausslemma2d  15590  lgseisenlem4  15594  lgseisen  15595  lgsquad2lem1  15602  lgsquad3  15605  2lgslem3a1  15618  2lgslem3b1  15619  2lgslem3c1  15620  2lgslem3d1  15621  pwf1oexmid  16010  nninfsellemdc  16021  trilpolemlt1  16054  apdiff  16061  iswomninnlem  16062