Theorem dedth

Description: Weak deduction theorem that eliminates a hypothesis ph , making it become an antecedent. We assume that a proof exists for ph when the class variable A is replaced with a specific class B . The hypothesis ch should be assigned to the inference, and the inference hypothesis eliminated with elimhyp . If the inference has other hypotheses with class variable A , these can be kept by assigning keephyp to them. For more information, see the Weak Deduction Theorem page mmdeduction.html . (Contributed by NM, 15-May-1999)

	Ref	Expression
Hypotheses	dedth.1	|- ( A = if ( ph , A , B ) -> ( ps <-> ch ) )
	dedth.2	|- ch
Assertion	dedth	|- ( ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		dedth.1	|- ( A = if ( ph , A , B ) -> ( ps <-> ch ) )
2		dedth.2	|- ch
3		iftrue	|- ( ph -> if ( ph , A , B ) = A )
4	3	eqcomd	|- ( ph -> A = if ( ph , A , B ) )
5	4 1	syl	|- ( ph -> ( ps <-> ch ) )
6	2 5	mpbiri	|- ( ph -> ps )