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\left(\phi ,A,B\right)\to \left(\psi \leftrightarrow \chi \right)$$
	dedth.2	$$⊢\chi$$
Assertion	dedth	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		dedth.1	$$⊢A=if\left(\phi ,A,B\right)\to \left(\psi \leftrightarrow \chi \right)$$
2		dedth.2	$$⊢\chi$$
3		iftrue	$$⊢\phi \to if\left(\phi ,A,B\right)=A$$
4	3	eqcomd	$$⊢\phi \to A=if\left(\phi ,A,B\right)$$
5	4 1	syl	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
6	2 5	mpbiri	$$⊢\phi \to \psi$$