Metamath Proof Explorer

Theorem 3impa

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995) (Revised to shorten 3imp by Wolf Lammen, 20-Jun-2022.)

Ref Expression
Hypothesis 3impa.1 φ ψ χ θ
Assertion 3impa φ ψ χ θ


Step Hyp Ref Expression
1 3impa.1 φ ψ χ θ
2 df-3an φ ψ χ φ ψ χ
3 2 1 sylbi φ ψ χ θ