Theorem ifpxorcor

Description: Corollary of commutation of biconditional. (Contributed by RP, 25-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		ifpbicor	⊢ ( if- ( 𝜑 , ¬ 𝜓 , ¬ ¬ 𝜓 ) ↔ if- ( ¬ 𝜓 , 𝜑 , ¬ 𝜑 ) )
2		notnotb	⊢ ( 𝜓 ↔ ¬ ¬ 𝜓 )
3		ifpbi3	⊢ ( ( 𝜓 ↔ ¬ ¬ 𝜓 ) → ( if- ( 𝜑 , ¬ 𝜓 , 𝜓 ) ↔ if- ( 𝜑 , ¬ 𝜓 , ¬ ¬ 𝜓 ) ) )
4	2 3	ax-mp	⊢ ( if- ( 𝜑 , ¬ 𝜓 , 𝜓 ) ↔ if- ( 𝜑 , ¬ 𝜓 , ¬ ¬ 𝜓 ) )
5		ifpn	⊢ ( if- ( 𝜓 , ¬ 𝜑 , 𝜑 ) ↔ if- ( ¬ 𝜓 , 𝜑 , ¬ 𝜑 ) )
6	1 4 5	3bitr4i	⊢ ( if- ( 𝜑 , ¬ 𝜓 , 𝜓 ) ↔ if- ( 𝜓 , ¬ 𝜑 , 𝜑 ) )