Theorem dedlema 569

Description: Lemma for weak deduction theorem.

Assertion

Ref	Expression
dedlema	⊢ (φ → (ψ ↔ ((ψ ∧ φ) ∨ (χ ∧ ¬ φ))))

Proof of Theorem dedlema

Step	Hyp	Ref	Expression
1		orc 225	. . . 4 ⊢ (ψ → (ψ ∨ (χ ∧ ¬ φ)))
2	1	a1i 7	. . 3 ⊢ (φ → (ψ → (ψ ∨ (χ ∧ ¬ φ))))
3		idd 11	. . . 4 ⊢ (φ → (ψ → ψ))
4		pm2.24 72	. . . . 5 ⊢ (φ → (¬ φ → ψ))
5	4	adantld 307	. . . 4 ⊢ (φ → ((χ ∧ ¬ φ) → ψ))
6	3, 5	jaod 329	. . 3 ⊢ (φ → ((ψ ∨ (χ ∧ ¬ φ)) → ψ))
7	2, 6	impbid 397	. 2 ⊢ (φ → (ψ ↔ (ψ ∨ (χ ∧ ¬ φ))))
8		iba 486	. . 3 ⊢ (φ → (ψ ↔ (ψ ∧ φ)))
9	8	orbi1d 467	. 2 ⊢ (φ → ((ψ ∨ (χ ∧ ¬ φ)) ↔ ((ψ ∧ φ) ∨ (χ ∧ ¬ φ))))
10	7, 9	bitrd 406	1 ⊢ (φ → (ψ ↔ ((ψ ∧ φ) ∨ (χ ∧ ¬ φ))))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∨ wo 195   ∧ wa 196

This theorem is referenced by:  elimh 571  dedt 572  consensus 574  iftrue 1780

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198

metamath.org