Metamath Proof Explorer

Theorem frege9

Description: Closed form of syl with swapped antecedents. This proposition differs from frege5 only in an unessential way. Identical to imim1 . Proposition 9 of Frege1879 p. 35. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege9 φ ψ ψ χ φ χ


Step Hyp Ref Expression
1 frege5 ψ χ φ ψ φ χ
2 ax-frege8 ψ χ φ ψ φ χ φ ψ ψ χ φ χ
3 1 2 ax-mp φ ψ ψ χ φ χ