Theorem dedth2v

Description: Weak deduction theorem for eliminating a hypothesis with 2 class variables. Note: if the hypothesis can be separated into two hypotheses, each with one class variable, then dedth2h is simpler to use. See also comments in dedth . (Contributed by NM, 13-Aug-1999) (Proof shortened by Eric Schmidt, 28-Jul-2009)

	Ref	Expression
Hypotheses	dedth2v.1	|- ( A = if ( ph , A , C ) -> ( ps <-> ch ) )
	dedth2v.2	|- ( B = if ( ph , B , D ) -> ( ch <-> th ) )
	dedth2v.3	|- th
Assertion	dedth2v	|- ( ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		dedth2v.1	|- ( A = if ( ph , A , C ) -> ( ps <-> ch ) )
2		dedth2v.2	|- ( B = if ( ph , B , D ) -> ( ch <-> th ) )
3		dedth2v.3	|- th
4	1 2 3	dedth2h	|- ( ( ph /\ ph ) -> ps )
5	4	anidms	|- ( ph -> ps )