Metamath Proof Explorer


Theorem imim2

Description: A closed form of syllogism (see syl ). Theorem *2.05 of WhiteheadRussell p. 100. Its associated inference is imim2i . Its associated deduction is imim2d . An alternate proof from more basic results is given by ax-1 followed by a2d . (Contributed by NM, 29-Dec-1992) (Proof shortened by Wolf Lammen, 6-Sep-2012)

Ref Expression
Assertion imim2 φ ψ χ φ χ ψ

Proof

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