Theorem pm11.59

Description: Theorem *11.59 in WhiteheadRussell p. 165. (Contributed by Andrew Salmon, 25-May-2011)

	Ref	Expression
Assertion	pm11.59	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ∀ 𝑦 ∀ 𝑥 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑦 ( 𝜑 → 𝜓 )
2	1	nfal	⊢ Ⅎ 𝑦 ∀ 𝑥 ( 𝜑 → 𝜓 )
3		sp	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) )
4		spsbim	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
5	3 4	anim12d	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ) )
6	5	axc4i	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ∀ 𝑥 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ) )
7	2 6	alrimi	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ∀ 𝑦 ∀ 𝑥 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ) )