This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝜓 , 𝐴 , 𝐵 ) )