Theorem ififcom

Description: Commute two nested conditionals. (Contributed by Thierry Arnoux, 4-May-2026)

	Ref	Expression
Assertion	ififcom	⊢ if ( 𝜑 , if ( 𝜓 , 𝐴 , 𝐵 ) , 𝐵 ) = if ( 𝜓 , if ( 𝜑 , 𝐴 , 𝐵 ) , 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ancom	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜓 ∧ 𝜑 ) )
2		ifbi	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜓 ∧ 𝜑 ) ) → if ( ( 𝜑 ∧ 𝜓 ) , 𝐴 , 𝐵 ) = if ( ( 𝜓 ∧ 𝜑 ) , 𝐴 , 𝐵 ) )
3	1 2	ax-mp	⊢ if ( ( 𝜑 ∧ 𝜓 ) , 𝐴 , 𝐵 ) = if ( ( 𝜓 ∧ 𝜑 ) , 𝐴 , 𝐵 )
4		ifan	⊢ if ( ( 𝜑 ∧ 𝜓 ) , 𝐴 , 𝐵 ) = if ( 𝜑 , if ( 𝜓 , 𝐴 , 𝐵 ) , 𝐵 )
5		ifan	⊢ if ( ( 𝜓 ∧ 𝜑 ) , 𝐴 , 𝐵 ) = if ( 𝜓 , if ( 𝜑 , 𝐴 , 𝐵 ) , 𝐵 )
6	3 4 5	3eqtr3i	⊢ if ( 𝜑 , if ( 𝜓 , 𝐴 , 𝐵 ) , 𝐵 ) = if ( 𝜓 , if ( 𝜑 , 𝐴 , 𝐵 ) , 𝐵 )