Metamath Proof Explorer


Theorem imim1

Description: A closed form of syllogism (see syl ). Theorem *2.06 of WhiteheadRussell p. 100. Its associated inference is imim1i . (Contributed by NM, 29-Dec-1992) (Proof shortened by Wolf Lammen, 25-May-2013)

Ref Expression
Assertion imim1 φ ψ ψ χ φ χ

Proof

Step Hyp Ref Expression
1 id φ ψ φ ψ
2 1 imim1d φ ψ ψ χ φ χ