Theorem dedth2h

Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v but requires that each hypothesis have exactly one class variable. See also comments in dedth . (Contributed by NM, 15-May-1999)

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

Proof

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