Theorem ifpn

Description: Conditional operator for the negation of a proposition. (Contributed by BJ, 30-Sep-2019) (Proof shortened by Wolf Lammen, 5-May-2024)

	Ref	Expression
Assertion	ifpn	|- ( if- ( ph , ps , ch ) <-> if- ( -. ph , ch , ps ) )

Proof

Step	Hyp	Ref	Expression
1		ancom	|- ( ( ( -. ph \/ ps ) /\ ( -. ph -> ch ) ) <-> ( ( -. ph -> ch ) /\ ( -. ph \/ ps ) ) )
2		dfifp5	|- ( if- ( ph , ps , ch ) <-> ( ( -. ph \/ ps ) /\ ( -. ph -> ch ) ) )
3		dfifp3	|- ( if- ( -. ph , ch , ps ) <-> ( ( -. ph -> ch ) /\ ( -. ph \/ ps ) ) )
4	1 2 3	3bitr4i	|- ( if- ( ph , ps , ch ) <-> if- ( -. ph , ch , ps ) )