Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Short Studies
Additional work on conditional logical operator
ifpnot23d
Next ⟩
ifpdfnan
Metamath Proof Explorer
Ascii
Unicode
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-
φ
ψ
χ