Theorem sbimi 1537

Description: Infer substitution into antecedent and consequent of an implication.

Hypothesis

Ref	Expression
sbimi.1	|- (ph -> ps)

Assertion

Ref	Expression
sbimi	|- ([y / x]ph -> [y / x]ps)

Proof of Theorem sbimi

Step	Hyp	Ref	Expression
1		sbimi.1	. . . 4 |- (ph -> ps)
2	1	imim2i 11	. . 3 |- ((x = y -> ph) -> (x = y -> ps))
3	1	anim2i 362	. . . 4 |- ((x = y /\ ph) -> (x = y /\ ps))
4	3	eximi 1387	. . 3 |- (E.x(x = y /\ ph) -> E.x(x = y /\ ps))
5	2, 4	anim12i 360	. 2 |- (((x = y -> ph) /\ E.x(x = y /\ ph)) -> ((x = y -> ps) /\ E.x(x = y /\ ps)))
6		df-sb 1536	. 2 |- ([y / x]ph <-> ((x = y -> ph) /\ E.x(x = y /\ ph)))
7		df-sb 1536	. 2 |- ([y / x]ps <-> ((x = y -> ps) /\ E.x(x = y /\ ps)))
8	5, 6, 7	3imtr4i 236	1 |- ([y / x]ph -> [y / x]ps)

Syntax hints:   -> wi 3   /\ wa 240  E.wex 1326  [wsbc 1534

This theorem is referenced by:  sbbii 1538  sb6f 1570  hbsb3 1575  sbi2 1603  hbsb4t 1621  sbco 1625  sbidm 1627  equsb3lemOLD 1716  elsb3 1718  elsb3OLD 1719  elsb4 1720  elsb4OLD 1721  sbal1 1737  sbal 1738  eqsb3lemOLD 1988  clelsb3 1990  clelsb3OLD 1991  tfinds2 3947  csbfsum 8287  bnj1483 13160  firnfi3 15743

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536

Copyright terms: Public domain