Theorem dedt

Description: The weak deduction theorem. For more information, see the Weak Deduction Theorem page mmdeduction.html . (Contributed by NM, 26-Jun-2002) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019) Commute consequent. (Revised by Steven Nguyen, 27-Apr-2023)

	Ref	Expression
Hypotheses	dedt.1	⊢ ( ( if- ( 𝜒 , 𝜑 , 𝜓 ) ↔ 𝜑 ) → ( 𝜏 ↔ 𝜃 ) )
	dedt.2	⊢ 𝜏
Assertion	dedt	⊢ ( 𝜒 → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		dedt.1	⊢ ( ( if- ( 𝜒 , 𝜑 , 𝜓 ) ↔ 𝜑 ) → ( 𝜏 ↔ 𝜃 ) )
2		dedt.2	⊢ 𝜏
3		ifptru	⊢ ( 𝜒 → ( if- ( 𝜒 , 𝜑 , 𝜓 ) ↔ 𝜑 ) )
4	2 1	mpbii	⊢ ( ( if- ( 𝜒 , 𝜑 , 𝜓 ) ↔ 𝜑 ) → 𝜃 )
5	3 4	syl	⊢ ( 𝜒 → 𝜃 )