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  5154  relcoi2  5292  supp0  6437  tfrlemi14d  6563  tfri1dALT  6581  mapsncnv  6929  findcard2d  7147  findcard2sd  7148  ac6sfi  7154  xpfi  7191  fifo  7266  updjudhcoinlf  7370  updjudhcoinrg  7371  updjud  7372  casefun  7375  omp1eomlem  7384  difinfsnlem  7389  djufun  7394  ctm  7399  ismkvnex  7445  cauappcvgprlemladd  7969  caucvgprprlemmu  8006  caucvgsrlemfv  8102  recidpirqlemcalc  8168  recidpirq  8169  axaddf  8179  axmulf  8180  xaddpnf1  10175  fldiv4lem1div2  10663  q0mod  10713  q1mod  10714  mulp1mod1  10723  m1modnnsub1  10728  modqm1p1mod0  10733  modqltm1p1mod  10734  bcval5  11121  swrd0g  11345  negfi  11906  xrmaxadd  11939  fprodle  12319  fprodmodd  12320  ege2le3  12350  sinltxirr  12440  p1modz1  12473  moddvds  12478  fsumdvds  12521  oddnn02np1  12559  oddge22np1  12560  evennn02n  12561  evennn2n  12562  bitsinv1lem  12640  3lcm2e6woprm  12776  6lcm4e12  12777  isprm6  12837  sqrt2irraplemnn  12869  fermltl  12924  phisum  12931  odzdvds  12936  reumodprminv  12944  pceu  12986  pcaddlem  13030  pcadd  13031  modxai  13107  modsubi  13110  ballotfilemofi  13131  ennnfonelemp1  13146  ennnfonelemkh  13152  ennnfonelemex  13154  exmidunben  13166  ssomct  13185  ssnnctlemct  13186  strslfv  13246  strleund  13305  prdsval  13475  prdsidlem  13649  pws0g  13653  idmhm  13671  mulgneg2  13862  gsumfzfsumlemm  14722  dvdsrzring  14738  expghmap  14742  zndvds  14784  cnbl0  15386  negfcncf  15458  cnrehmeocntop  15462  divcncfap  15466  dvidlemap  15543  dvidrelem  15544  dvidsslem  15545  dvid  15547  dvidre  15549  dvmulxxbr  15554  dvexp  15563  plycjlemc  15612  plycj  15613  dvply1  15617  dvply2g  15618  sincn  15621  coscn  15622  coseq0q4123  15686  tangtx  15690  cosordlem  15701  wilthlem1  15835  1sgm2ppw  15850  perfectlem2  15855  lgslem1  15860  lgsvalmod  15879  lgsmod  15886  lgsdir2lem5  15892  lgsne0  15898  gausslemma2d  15929  lgseisenlem4  15933  lgseisen  15934  lgsquad2lem1  15941  lgsquad3  15944  2lgslem3a1  15957  2lgslem3b1  15958  2lgslem3c1  15959  2lgslem3d1  15960  uspgr2wlkeq  16347  konigsberglem2  16471  pwf1oexmid  16760  nninfsellemdc  16775  trilpolemlt1  16812  apdiff  16819  qdiff  16820  iswomninnlem  16821  gfsumz  16855