Theorem ififcom

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

	Ref	Expression
Assertion	ififcom	|- if ( ph , if ( ps , A , B ) , B ) = if ( ps , if ( ph , A , B ) , B )

Proof

Step	Hyp	Ref	Expression
1		ancom	|- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
2		ifbi	|- ( ( ( ph /\ ps ) <-> ( ps /\ ph ) ) -> if ( ( ph /\ ps ) , A , B ) = if ( ( ps /\ ph ) , A , B ) )
3	1 2	ax-mp	|- if ( ( ph /\ ps ) , A , B ) = if ( ( ps /\ ph ) , A , B )
4		ifan	|- if ( ( ph /\ ps ) , A , B ) = if ( ph , if ( ps , A , B ) , B )
5		ifan	|- if ( ( ps /\ ph ) , A , B ) = if ( ps , if ( ph , A , B ) , B )
6	3 4 5	3eqtr3i	|- if ( ph , if ( ps , A , B ) , B ) = if ( ps , if ( ph , A , B ) , B )