Theorem ralimi2

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004)

	Ref	Expression
Hypothesis	ralimi2.1	|- ( ( x e. A -> ph ) -> ( x e. B -> ps ) )
Assertion	ralimi2	|- ( A. x e. A ph -> A. x e. B ps )

Proof

Step	Hyp	Ref	Expression
1		ralimi2.1	|- ( ( x e. A -> ph ) -> ( x e. B -> ps ) )
2	1	alimi	|- ( A. x ( x e. A -> ph ) -> A. x ( x e. B -> ps ) )
3		df-ral	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
4		df-ral	|- ( A. x e. B ps <-> A. x ( x e. B -> ps ) )
5	2 3 4	3imtr4i	|- ( A. x e. A ph -> A. x e. B ps )