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

Metamath Proof Explorer

Theorem spcdv

Description: Rule of specialization, using implicit substitution. Analogous to rspcdv . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	spcimdv.1	$⊢ φ \to A \in B$
	spcdv.2	$⊢ (φ \land x = A) \to (ψ \leftrightarrow χ)$
Assertion	spcdv	$⊢ φ \to (\forall x ψ \to χ)$

Step	Hyp	Ref	Expression
1		spcimdv.1	$⊢ φ \to A \in B$
2		spcdv.2	$⊢ (φ \land x = A) \to (ψ \leftrightarrow χ)$
3	2	biimpd	$⊢ (φ \land x = A) \to (ψ \to χ)$
4	1 3	spcimdv	$⊢ φ \to (\forall x ψ \to χ)$