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 φψψχφχ