This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbi2

Description: Introduction of implication into substitution. (Contributed by NM, 14-May-1993)

		Ref	Expression
	Assertion	sbi2	$⊢ ([y/ x] φ \to [y/ x] ψ) \to [y/ x] (φ \to ψ)$

Step	Hyp	Ref	Expression
1		sbn	$⊢ [y/ x] \neg φ \leftrightarrow \neg [y/ x] φ$
2		pm2.21	$⊢ \neg φ \to (φ \to ψ)$
3	2	sbimi	$⊢ [y/ x] \neg φ \to [y/ x] (φ \to ψ)$
4	1 3	sylbir	$⊢ \neg [y/ x] φ \to [y/ x] (φ \to ψ)$
5		ax-1	$⊢ ψ \to (φ \to ψ)$
6	5	sbimi	$⊢ [y/ x] ψ \to [y/ x] (φ \to ψ)$
7	4 6	ja	$⊢ ([y/ x] φ \to [y/ x] ψ) \to [y/ x] (φ \to ψ)$