Theorem dedth3h

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

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

Proof

Step	Hyp	Ref	Expression
1		dedth3h.1	|- ( A = if ( ph , A , D ) -> ( th <-> ta ) )
2		dedth3h.2	|- ( B = if ( ps , B , R ) -> ( ta <-> et ) )
3		dedth3h.3	|- ( C = if ( ch , C , S ) -> ( et <-> ze ) )
4		dedth3h.4	|- ze
5	1	imbi2d	|- ( A = if ( ph , A , D ) -> ( ( ( ps /\ ch ) -> th ) <-> ( ( ps /\ ch ) -> ta ) ) )
6	2 3 4	dedth2h	|- ( ( ps /\ ch ) -> ta )
7	5 6	dedth	|- ( ph -> ( ( ps /\ ch ) -> th ) )
8	7	3impib	|- ( ( ph /\ ps /\ ch ) -> th )