Metamath Proof Explorer


Theorem pm2.521g

Description: A general instance of Theorem *2.521 of WhiteheadRussell p. 107. (Contributed by BJ, 28-Oct-2023)

Ref Expression
Assertion pm2.521g ¬ φ ψ ψ χ

Proof

Step Hyp Ref Expression
1 conax1 ¬ φ ψ ¬ ψ
2 1 pm2.21d ¬ φ ψ ψ χ