Theorem ifpnot23

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

	Ref	Expression
Assertion	ifpnot23	⊢ ( ¬ if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		ianor	⊢ ( ¬ ( 𝜑 ∧ 𝜓 ) ↔ ( ¬ 𝜑 ∨ ¬ 𝜓 ) )
2		pm4.55	⊢ ( ¬ ( ¬ 𝜑 ∧ 𝜒 ) ↔ ( 𝜑 ∨ ¬ 𝜒 ) )
3	1 2	anbi12i	⊢ ( ( ¬ ( 𝜑 ∧ 𝜓 ) ∧ ¬ ( ¬ 𝜑 ∧ 𝜒 ) ) ↔ ( ( ¬ 𝜑 ∨ ¬ 𝜓 ) ∧ ( 𝜑 ∨ ¬ 𝜒 ) ) )
4		ioran	⊢ ( ¬ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ↔ ( ¬ ( 𝜑 ∧ 𝜓 ) ∧ ¬ ( ¬ 𝜑 ∧ 𝜒 ) ) )
5		dfifp4	⊢ ( if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜒 ) ↔ ( ( ¬ 𝜑 ∨ ¬ 𝜓 ) ∧ ( 𝜑 ∨ ¬ 𝜒 ) ) )
6	3 4 5	3bitr4i	⊢ ( ¬ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ↔ if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜒 ) )
7		df-ifp	⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
8	6 7	xchnxbir	⊢ ( ¬ if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜒 ) )