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  5129  relcoi2  5267  tfrlemi14d  6499  tfri1dALT  6517  mapsncnv  6864  findcard2d  7080  findcard2sd  7081  ac6sfi  7087  xpfi  7124  fifo  7179  updjudhcoinlf  7279  updjudhcoinrg  7280  updjud  7281  casefun  7284  omp1eomlem  7293  difinfsnlem  7298  djufun  7303  ctm  7308  ismkvnex  7354  cauappcvgprlemladd  7878  caucvgprprlemmu  7915  caucvgsrlemfv  8011  recidpirqlemcalc  8077  recidpirq  8078  axaddf  8088  axmulf  8089  xaddpnf1  10081  fldiv4lem1div2  10568  q0mod  10618  q1mod  10619  mulp1mod1  10628  m1modnnsub1  10633  modqm1p1mod0  10638  modqltm1p1mod  10639  bcval5  11026  swrd0g  11242  negfi  11790  xrmaxadd  11823  fprodle  12203  fprodmodd  12204  ege2le3  12234  sinltxirr  12324  p1modz1  12357  moddvds  12362  fsumdvds  12405  oddnn02np1  12443  oddge22np1  12444  evennn02n  12445  evennn2n  12446  bitsinv1lem  12524  3lcm2e6woprm  12660  6lcm4e12  12661  isprm6  12721  sqrt2irraplemnn  12753  fermltl  12808  phisum  12815  odzdvds  12820  reumodprminv  12828  pceu  12870  pcaddlem  12914  pcadd  12915  modxai  12991  modsubi  12994  ennnfonelemp1  13029  ennnfonelemkh  13035  ennnfonelemex  13037  exmidunben  13049  ssomct  13068  ssnnctlemct  13069  strslfv  13129  strleund  13188  prdsval  13358  prdsidlem  13532  pws0g  13536  idmhm  13554  mulgneg2  13745  gsumfzfsumlemm  14604  dvdsrzring  14620  expghmap  14624  zndvds  14666  cnbl0  15261  negfcncf  15333  cnrehmeocntop  15337  divcncfap  15341  dvidlemap  15418  dvidrelem  15419  dvidsslem  15420  dvid  15422  dvidre  15424  dvmulxxbr  15429  dvexp  15438  plycjlemc  15487  plycj  15488  dvply1  15492  dvply2g  15493  sincn  15496  coscn  15497  coseq0q4123  15561  tangtx  15565  cosordlem  15576  wilthlem1  15707  1sgm2ppw  15722  perfectlem2  15727  lgslem1  15732  lgsvalmod  15751  lgsmod  15758  lgsdir2lem5  15764  lgsne0  15770  gausslemma2d  15801  lgseisenlem4  15805  lgseisen  15806  lgsquad2lem1  15813  lgsquad3  15816  2lgslem3a1  15829  2lgslem3b1  15830  2lgslem3c1  15831  2lgslem3d1  15832  uspgr2wlkeq  16219  pwf1oexmid  16621  nninfsellemdc  16633  trilpolemlt1  16666  apdiff  16673  iswomninnlem  16674