Theorem dedlemb

Description: Lemma for weak deduction theorem. See also ifpfal . (Contributed by NM, 15-May-1999) (Proof shortened by Andrew Salmon, 7-May-2011)

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

Proof

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