Metamath Proof Explorer

Theorem frege6

Description: A closed form of imim2d which is a deduction adding nested antecedents. Proposition 6 of Frege1879 p. 33. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege6 ⊢ φ → ψ → χ → φ → θ → ψ → θ → χ

Proof

Step Hyp Ref Expression
1 frege5 ⊢ ψ → χ → θ → ψ → θ → χ
2 frege5 ⊢ ψ → χ → θ → ψ → θ → χ → φ → ψ → χ → φ → θ → ψ → θ → χ
3 1 2 ax-mp ⊢ φ → ψ → χ → φ → θ → ψ → θ → χ