Metamath Proof Explorer


Theorem ifpnot23d

Description: Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 ifpnot23 ¬ if- φ ¬ ψ ¬ χ if- φ ¬ ¬ ψ ¬ ¬ χ
2 notnotb ψ ¬ ¬ ψ
3 notnotb χ ¬ ¬ χ
4 ifpbi23 ψ ¬ ¬ ψ χ ¬ ¬ χ if- φ ψ χ if- φ ¬ ¬ ψ ¬ ¬ χ
5 2 3 4 mp2an if- φ ψ χ if- φ ¬ ¬ ψ ¬ ¬ χ
6 1 5 bitr4i ¬ if- φ ¬ ψ ¬ χ if- φ ψ χ