Metamath Proof Explorer


Syntax definition w-bnj17

Description: Extend wff notation with the 4-way conjunction. (New usage is discouraged.)

Ref Expression
Assertion w-bnj17 wff φ ψ χ θ