Theorem dedth4h

Description: Weak deduction theorem eliminating four hypotheses. See comments in dedth2h . (Contributed by NM, 16-May-1999)

	Ref	Expression
Hypotheses	dedth4h.1	|- ( A = if ( ph , A , R ) -> ( ta <-> et ) )
	dedth4h.2	|- ( B = if ( ps , B , S ) -> ( et <-> ze ) )
	dedth4h.3	|- ( C = if ( ch , C , F ) -> ( ze <-> si ) )
	dedth4h.4	|- ( D = if ( th , D , G ) -> ( si <-> rh ) )
	dedth4h.5	|- rh
Assertion	dedth4h	|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )

Proof

Step	Hyp	Ref	Expression
1		dedth4h.1	|- ( A = if ( ph , A , R ) -> ( ta <-> et ) )
2		dedth4h.2	|- ( B = if ( ps , B , S ) -> ( et <-> ze ) )
3		dedth4h.3	|- ( C = if ( ch , C , F ) -> ( ze <-> si ) )
4		dedth4h.4	|- ( D = if ( th , D , G ) -> ( si <-> rh ) )
5		dedth4h.5	|- rh
6	1	imbi2d	|- ( A = if ( ph , A , R ) -> ( ( ( ch /\ th ) -> ta ) <-> ( ( ch /\ th ) -> et ) ) )
7	2	imbi2d	|- ( B = if ( ps , B , S ) -> ( ( ( ch /\ th ) -> et ) <-> ( ( ch /\ th ) -> ze ) ) )
8	3 4 5	dedth2h	|- ( ( ch /\ th ) -> ze )
9	6 7 8	dedth2h	|- ( ( ph /\ ps ) -> ( ( ch /\ th ) -> ta ) )
10	9	imp	|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )