Theorem dedth4v

Description: Weak deduction theorem for eliminating a hypothesis with 4 class variables. See comments in dedth2v . (Contributed by NM, 21-Apr-2007) (Proof shortened by Eric Schmidt, 28-Jul-2009)

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

Proof

Step	Hyp	Ref	Expression
1		dedth4v.1	|- ( A = if ( ph , A , R ) -> ( ps <-> ch ) )
2		dedth4v.2	|- ( B = if ( ph , B , S ) -> ( ch <-> th ) )
3		dedth4v.3	|- ( C = if ( ph , C , T ) -> ( th <-> ta ) )
4		dedth4v.4	|- ( D = if ( ph , D , U ) -> ( ta <-> et ) )
5		dedth4v.5	|- et
6	1 2 3 4 5	dedth4h	|- ( ( ( ph /\ ph ) /\ ( ph /\ ph ) ) -> ps )
7	6	anidms	|- ( ( ph /\ ph ) -> ps )
8	7	anidms	|- ( ph -> ps )