Theorem dedlem0a 567

Description: Lemma for an alternate version of weak deduction theorem.

Assertion

Ref	Expression
dedlem0a	⊢ (φ → (ψ ↔ ((χ → φ) → (ψ ∧ φ))))

Proof of Theorem dedlem0a

Step	Hyp	Ref	Expression
1		ax-1 3	. . . 4 ⊢ (ψ → ((χ → φ) → ψ))
2	1	a1i 7	. . 3 ⊢ (φ → (ψ → ((χ → φ) → ψ)))
3		ax-1 3	. . . . 5 ⊢ (φ → (χ → φ))
4	3	syl4 19	. . . 4 ⊢ (((χ → φ) → ψ) → (φ → ψ))
5	4	com12 13	. . 3 ⊢ (φ → (((χ → φ) → ψ) → ψ))
6	2, 5	impbid 397	. 2 ⊢ (φ → (ψ ↔ ((χ → φ) → ψ)))
7		iba 486	. . 3 ⊢ (φ → (ψ ↔ (ψ ∧ φ)))
8	7	imbi2d 464	. 2 ⊢ (φ → (((χ → φ) → ψ) ↔ ((χ → φ) → (ψ ∧ φ))))
9	6, 8	bitrd 406	1 ⊢ (φ → (ψ ↔ ((χ → φ) → (ψ ∧ φ))))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196

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-an 198

metamath.org