Metamath Proof Explorer


Theorem ifpnotnotb

Description: Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020)

Ref Expression
Assertion ifpnotnotb if- φ ¬ ψ ¬ χ ¬ if- φ ψ χ

Proof

Step Hyp Ref Expression
1 ifpnot23 ¬ if- φ ψ χ if- φ ¬ ψ ¬ χ
2 1 bicomi if- φ ¬ ψ ¬ χ ¬ if- φ ψ χ