Theorem elimant 505

Description: Elimination of antecedents in an implication.

Assertion

Ref	Expression
elimant	⊢ (((φ → ψ) ∧ ((ψ → χ) → (φ → θ))) → (φ → (χ → θ)))

Proof of Theorem elimant

Step	Hyp	Ref	Expression
1		id 9	. . . . . . . . . . 11 ⊢ ((φ → ψ) → (φ → ψ))
2	1	impac 304	. . . . . . . . . 10 ⊢ (((φ → ψ) ∧ φ) → (ψ ∧ φ))
3		pm5.1 501	. . . . . . . . . 10 ⊢ ((ψ ∧ φ) → (ψ ↔ φ))
4	2, 3	syl 12	. . . . . . . . 9 ⊢ (((φ → ψ) ∧ φ) → (ψ ↔ φ))
5	4	imbi1d 465	. . . . . . . 8 ⊢ (((φ → ψ) ∧ φ) → ((ψ → χ) ↔ (φ → χ)))
6	5	imbi1d 465	. . . . . . 7 ⊢ (((φ → ψ) ∧ φ) → (((ψ → χ) → (φ → θ)) ↔ ((φ → χ) → (φ → θ))))
7	6	biimpd 135	. . . . . 6 ⊢ (((φ → ψ) ∧ φ) → (((ψ → χ) → (φ → θ)) → ((φ → χ) → (φ → θ))))
8	7	exp 291	. . . . 5 ⊢ ((φ → ψ) → (φ → (((ψ → χ) → (φ → θ)) → ((φ → χ) → (φ → θ)))))
9	8	com23 32	. . . 4 ⊢ ((φ → ψ) → (((ψ → χ) → (φ → θ)) → (φ → ((φ → χ) → (φ → θ)))))
10	9	imp 277	. . 3 ⊢ (((φ → ψ) ∧ ((ψ → χ) → (φ → θ))) → (φ → ((φ → χ) → (φ → θ))))
11		imdi 147	. . 3 ⊢ ((φ → (χ → θ)) ↔ ((φ → χ) → (φ → θ)))
12	10, 11	syl6ibr 186	. 2 ⊢ (((φ → ψ) ∧ ((ψ → χ) → (φ → θ))) → (φ → (φ → (χ → θ))))
13	12	pm2.43d 59	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