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  5157  relcoi2  5295  supp0  6440  tfrlemi14d  6566  tfri1dALT  6584  mapsncnv  6932  findcard2d  7150  findcard2sd  7151  ac6sfi  7157  xpfi  7194  fifo  7269  updjudhcoinlf  7373  updjudhcoinrg  7374  updjud  7375  casefun  7378  omp1eomlem  7387  difinfsnlem  7392  djufun  7397  ctm  7402  ismkvnex  7448  cauappcvgprlemladd  7978  caucvgprprlemmu  8015  caucvgsrlemfv  8111  recidpirqlemcalc  8177  recidpirq  8178  axaddf  8188  axmulf  8189  xaddpnf1  10185  fldiv4lem1div2  10674  q0mod  10724  q1mod  10725  mulp1mod1  10734  m1modnnsub1  10739  modqm1p1mod0  10744  modqltm1p1mod  10745  bcval5  11133  hashmap  11200  swrd0g  11360  negfi  11921  xrmaxadd  11954  fprodle  12334  fprodmodd  12335  ege2le3  12365  sinltxirr  12455  p1modz1  12488  moddvds  12493  fsumdvds  12536  oddnn02np1  12574  oddge22np1  12575  evennn02n  12576  evennn2n  12577  bitsinv1lem  12655  3lcm2e6woprm  12791  6lcm4e12  12792  isprm6  12852  sqrt2irraplemnn  12884  fermltl  12939  phisum  12946  odzdvds  12951  reumodprminv  12959  pceu  13001  pcaddlem  13045  pcadd  13046  modxai  13122  modsubi  13125  ballotfilemofi  13146  ballotfilem2  13153  ballotfilemfmpn  13159  ennnfonelemp1  13178  ennnfonelemkh  13184  ennnfonelemex  13186  exmidunben  13198  ssomct  13217  ssnnctlemct  13218  strslfv  13278  strleund  13337  prdsval  13507  prdsidlem  13681  pws0g  13685  idmhm  13703  mulgneg2  13894  gsumfzfsumlemm  14784  dvdsrzring  14800  expghmap  14804  zndvds  14846  cnbl0  15448  negfcncf  15520  cnrehmeocntop  15524  divcncfap  15528  dvidlemap  15605  dvidrelem  15606  dvidsslem  15607  dvid  15609  dvidre  15611  dvmulxxbr  15616  dvexp  15625  plycjlemc  15674  plycj  15675  dvply1  15679  dvply2g  15680  sincn  15683  coscn  15684  coseq0q4123  15748  tangtx  15752  cosordlem  15763  wilthlem1  15897  1sgm2ppw  15912  perfectlem2  15917  lgslem1  15922  lgsvalmod  15941  lgsmod  15948  lgsdir2lem5  15954  lgsne0  15960  gausslemma2d  15991  lgseisenlem4  15995  lgseisen  15996  lgsquad2lem1  16003  lgsquad3  16006  2lgslem3a1  16019  2lgslem3b1  16020  2lgslem3c1  16021  2lgslem3d1  16022  uspgr2wlkeq  16409  konigsberglem2  16533  pwf1oexmid  16822  nninfsellemdc  16837  trilpolemlt1  16874  apdiff  16881  qdiff  16882  iswomninnlem  16883  gfsumz  16918