Theorem ifbi

Description: Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004)

	Ref	Expression
Assertion	ifbi	⊢ ( ( 𝜑 ↔ 𝜓 ) → if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐴 , 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dfbi3	⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ ¬ 𝜓 ) ) )
2		iftrue	⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 )
3		iftrue	⊢ ( 𝜓 → if ( 𝜓 , 𝐴 , 𝐵 ) = 𝐴 )
4	3	eqcomd	⊢ ( 𝜓 → 𝐴 = if ( 𝜓 , 𝐴 , 𝐵 ) )
5	2 4	sylan9eq	⊢ ( ( 𝜑 ∧ 𝜓 ) → if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐴 , 𝐵 ) )
6		iffalse	⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 )
7		iffalse	⊢ ( ¬ 𝜓 → if ( 𝜓 , 𝐴 , 𝐵 ) = 𝐵 )
8	7	eqcomd	⊢ ( ¬ 𝜓 → 𝐵 = if ( 𝜓 , 𝐴 , 𝐵 ) )
9	6 8	sylan9eq	⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐴 , 𝐵 ) )
10	5 9	jaoi	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ ¬ 𝜓 ) ) → if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐴 , 𝐵 ) )
11	1 10	sylbi	⊢ ( ( 𝜑 ↔ 𝜓 ) → if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐴 , 𝐵 ) )