Theorem dedth3v

Description: Weak deduction theorem for eliminating a hypothesis with 3 class variables. See comments in dedth2v . (Contributed by NM, 13-Aug-1999) (Proof shortened by Eric Schmidt, 28-Jul-2009)

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

Proof

Step	Hyp	Ref	Expression
1		dedth3v.1	|- ( A = if ( ph , A , D ) -> ( ps <-> ch ) )
2		dedth3v.2	|- ( B = if ( ph , B , R ) -> ( ch <-> th ) )
3		dedth3v.3	|- ( C = if ( ph , C , S ) -> ( th <-> ta ) )
4		dedth3v.4	|- ta
5	1 2 3 4	dedth3h	|- ( ( ph /\ ph /\ ph ) -> ps )
6	5	3anidm12	|- ( ( ph /\ ph ) -> ps )
7	6	anidms	|- ( ph -> ps )