Theorem dedlema

Description: Lemma for weak deduction theorem. See also ifptru . (Contributed by NM, 26-Jun-2002) (Proof shortened by Andrew Salmon, 7-May-2011)

	Ref	Expression
Assertion	dedlema	⊢ ( 𝜑 → ( 𝜓 ↔ ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		orc	⊢ ( ( 𝜓 ∧ 𝜑 ) → ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) )
2	1	expcom	⊢ ( 𝜑 → ( 𝜓 → ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) )
3		simpl	⊢ ( ( 𝜓 ∧ 𝜑 ) → 𝜓 )
4	3	a1i	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜑 ) → 𝜓 ) )
5		pm2.24	⊢ ( 𝜑 → ( ¬ 𝜑 → 𝜓 ) )
6	5	adantld	⊢ ( 𝜑 → ( ( 𝜒 ∧ ¬ 𝜑 ) → 𝜓 ) )
7	4 6	jaod	⊢ ( 𝜑 → ( ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) → 𝜓 ) )
8	2 7	impbid	⊢ ( 𝜑 → ( 𝜓 ↔ ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) )