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	⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
	dedth.2	⊢ 𝜒
Assertion	dedth	⊢ ( 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		dedth.1	⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
2		dedth.2	⊢ 𝜒
3		iftrue	⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 )
4	3	eqcomd	⊢ ( 𝜑 → 𝐴 = if ( 𝜑 , 𝐴 , 𝐵 ) )
5	4 1	syl	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
6	2 5	mpbiri	⊢ ( 𝜑 → 𝜓 )