Theorem sbimi 1177

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

Hypothesis

Ref	Expression
sbimi.1	⊢ (φ → ψ)

Assertion

Ref	Expression
sbimi	⊢ ([y / x]φ → [y / x]ψ)

Proof of Theorem sbimi

Step	Hyp	Ref	Expression
1		sbimi.1	. . . 4 ⊢ (φ → ψ)
2	1	imim2i 17	. . 3 ⊢ ((x = y → φ) → (x = y → ψ))
3	1	anim2i 335	. . . 4 ⊢ ((x = y ⋀ φ) → (x = y ⋀ ψ))
4	3	19.22i 1044	. . 3 ⊢ (∃x(x = y ⋀ φ) → ∃x(x = y ⋀ ψ))
5	2, 4	anim12i 333	. 2 ⊢ (((x = y → φ) ⋀ ∃x(x = y ⋀ φ)) → ((x = y → ψ) ⋀ ∃x(x = y ⋀ ψ)))
6		df-sb 1176	. 2 ⊢ ([y / x]φ ↔ ((x = y → φ) ⋀ ∃x(x = y ⋀ φ)))
7		df-sb 1176	. 2 ⊢ ([y / x]ψ ↔ ((x = y → ψ) ⋀ ∃x(x = y ⋀ ψ)))
8	5, 6, 7	3imtr4i 219	1 ⊢ ([y / x]φ → [y / x]ψ)

Syntax hints:   → wi 3   ⋀ wa 223  ∃wex 984  [wsbc 1174

This theorem is referenced by:  sbbii 1178  sb6f 1205  hbsb3 1210  sbi2 1237  sbco 1256  equsb3lem 1333  elsb3 1335  sbal1 1350  sbal 1351  tfinds2 3181  csbfsum 7059

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 967  ax-4 977  ax-5o 979

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 985  df-sb 1176

Copyright terms: Public domain