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  5131  relcoi2  5269  tfrlemi14d  6504  tfri1dALT  6522  mapsncnv  6869  findcard2d  7085  findcard2sd  7086  ac6sfi  7092  xpfi  7129  fifo  7184  updjudhcoinlf  7284  updjudhcoinrg  7285  updjud  7286  casefun  7289  omp1eomlem  7298  difinfsnlem  7303  djufun  7308  ctm  7313  ismkvnex  7359  cauappcvgprlemladd  7883  caucvgprprlemmu  7920  caucvgsrlemfv  8016  recidpirqlemcalc  8082  recidpirq  8083  axaddf  8093  axmulf  8094  xaddpnf1  10086  fldiv4lem1div2  10573  q0mod  10623  q1mod  10624  mulp1mod1  10633  m1modnnsub1  10638  modqm1p1mod0  10643  modqltm1p1mod  10644  bcval5  11031  swrd0g  11250  negfi  11811  xrmaxadd  11844  fprodle  12224  fprodmodd  12225  ege2le3  12255  sinltxirr  12345  p1modz1  12378  moddvds  12383  fsumdvds  12426  oddnn02np1  12464  oddge22np1  12465  evennn02n  12466  evennn2n  12467  bitsinv1lem  12545  3lcm2e6woprm  12681  6lcm4e12  12682  isprm6  12742  sqrt2irraplemnn  12774  fermltl  12829  phisum  12836  odzdvds  12841  reumodprminv  12849  pceu  12891  pcaddlem  12935  pcadd  12936  modxai  13012  modsubi  13015  ennnfonelemp1  13050  ennnfonelemkh  13056  ennnfonelemex  13058  exmidunben  13070  ssomct  13089  ssnnctlemct  13090  strslfv  13150  strleund  13209  prdsval  13379  prdsidlem  13553  pws0g  13557  idmhm  13575  mulgneg2  13766  gsumfzfsumlemm  14625  dvdsrzring  14641  expghmap  14645  zndvds  14687  cnbl0  15287  negfcncf  15359  cnrehmeocntop  15363  divcncfap  15367  dvidlemap  15444  dvidrelem  15445  dvidsslem  15446  dvid  15448  dvidre  15450  dvmulxxbr  15455  dvexp  15464  plycjlemc  15513  plycj  15514  dvply1  15518  dvply2g  15519  sincn  15522  coscn  15523  coseq0q4123  15587  tangtx  15591  cosordlem  15602  wilthlem1  15733  1sgm2ppw  15748  perfectlem2  15753  lgslem1  15758  lgsvalmod  15777  lgsmod  15784  lgsdir2lem5  15790  lgsne0  15796  gausslemma2d  15827  lgseisenlem4  15831  lgseisen  15832  lgsquad2lem1  15839  lgsquad3  15842  2lgslem3a1  15855  2lgslem3b1  15856  2lgslem3c1  15857  2lgslem3d1  15858  uspgr2wlkeq  16245  konigsberglem2  16369  pwf1oexmid  16660  nninfsellemdc  16675  trilpolemlt1  16712  apdiff  16719  qdiff  16720  iswomninnlem  16721