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  5062  relcoi2  5200  tfrlemi14d  6391  tfri1dALT  6409  mapsncnv  6754  findcard2d  6952  findcard2sd  6953  ac6sfi  6959  xpfi  6993  fifo  7046  updjudhcoinlf  7146  updjudhcoinrg  7147  updjud  7148  casefun  7151  omp1eomlem  7160  difinfsnlem  7165  djufun  7170  ctm  7175  ismkvnex  7221  cauappcvgprlemladd  7725  caucvgprprlemmu  7762  caucvgsrlemfv  7858  recidpirqlemcalc  7924  recidpirq  7925  axaddf  7935  axmulf  7936  xaddpnf1  9921  fldiv4lem1div2  10397  q0mod  10447  q1mod  10448  mulp1mod1  10457  m1modnnsub1  10462  modqm1p1mod0  10467  modqltm1p1mod  10468  bcval5  10855  negfi  11393  xrmaxadd  11426  fprodle  11805  fprodmodd  11806  ege2le3  11836  sinltxirr  11926  p1modz1  11959  moddvds  11964  fsumdvds  12007  oddnn02np1  12045  oddge22np1  12046  evennn02n  12047  evennn2n  12048  3lcm2e6woprm  12254  6lcm4e12  12255  isprm6  12315  sqrt2irraplemnn  12347  fermltl  12402  phisum  12409  odzdvds  12414  reumodprminv  12422  pceu  12464  pcaddlem  12508  pcadd  12509  modxai  12585  modsubi  12588  ennnfonelemp1  12623  ennnfonelemkh  12629  ennnfonelemex  12631  exmidunben  12643  ssomct  12662  ssnnctlemct  12663  strslfv  12723  strleund  12781  idmhm  13101  mulgneg2  13286  gsumfzfsumlemm  14143  dvdsrzring  14159  expghmap  14163  zndvds  14205  cnbl0  14770  negfcncf  14842  cnrehmeocntop  14846  divcncfap  14850  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvid  14931  dvidre  14933  dvmulxxbr  14938  dvexp  14947  plycjlemc  14996  plycj  14997  dvply1  15001  dvply2g  15002  sincn  15005  coscn  15006  coseq0q4123  15070  tangtx  15074  cosordlem  15085  wilthlem1  15216  1sgm2ppw  15231  perfectlem2  15236  lgslem1  15241  lgsvalmod  15260  lgsmod  15267  lgsdir2lem5  15273  lgsne0  15279  gausslemma2d  15310  lgseisenlem4  15314  lgseisen  15315  lgsquad2lem1  15322  lgsquad3  15325  2lgslem3a1  15338  2lgslem3b1  15339  2lgslem3c1  15340  2lgslem3d1  15341  pwf1oexmid  15644  nninfsellemdc  15654  trilpolemlt1  15685  apdiff  15692  iswomninnlem  15693