Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Short Studies
Additional work on conditional logical operator
ifpnorcor
Next ⟩
ifpnancor
Metamath Proof Explorer
Ascii
Unicode
Theorem
ifpnorcor
Description:
Corollary of commutation of nor.
(Contributed by
RP
, 25-Apr-2020)
Ref
Expression
Assertion
ifpnorcor
⊢
if-
φ
¬
φ
¬
ψ
↔
if-
ψ
¬
ψ
¬
φ
Proof
Step
Hyp
Ref
Expression
1
ifporcor
⊢
if-
φ
φ
ψ
↔
if-
ψ
ψ
φ
2
1
notbii
⊢
¬
if-
φ
φ
ψ
↔
¬
if-
ψ
ψ
φ
3
ifpnot23
⊢
¬
if-
φ
φ
ψ
↔
if-
φ
¬
φ
¬
ψ
4
ifpnot23
⊢
¬
if-
ψ
ψ
φ
↔
if-
ψ
¬
ψ
¬
φ
5
2
3
4
3bitr3i
⊢
if-
φ
¬
φ
¬
ψ
↔
if-
ψ
¬
ψ
¬
φ