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

Metamath Proof Explorer

Theorem ifeq12da

Description: Equivalence deduction for conditional operators. (Contributed by Wolf Lammen, 24-Jun-2021)

Ref Expression
Hypotheses ifeq12da.1 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 = 𝐶 )
ifeq12da.2 ⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝐵 = 𝐷 )
Assertion ifeq12da ( 𝜑 → if ( 𝜓 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐶 , 𝐷 ) )

Proof

Step Hyp Ref Expression
1 ifeq12da.1 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 = 𝐶 )
2 ifeq12da.2 ⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝐵 = 𝐷 )
3 1 ifeq1da ⊢ ( 𝜑 → if ( 𝜓 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐶 , 𝐵 ) )
4 iftrue ⊢ ( 𝜓 → if ( 𝜓 , 𝐶 , 𝐵 ) = 𝐶 )
5 iftrue ⊢ ( 𝜓 → if ( 𝜓 , 𝐶 , 𝐷 ) = 𝐶 )
6 4 5 eqtr4d ⊢ ( 𝜓 → if ( 𝜓 , 𝐶 , 𝐵 ) = if ( 𝜓 , 𝐶 , 𝐷 ) )
7 3 6 sylan9eq ⊢ ( ( 𝜑 ∧ 𝜓 ) → if ( 𝜓 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐶 , 𝐷 ) )
8 2 ifeq2da ⊢ ( 𝜑 → if ( 𝜓 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐴 , 𝐷 ) )
9 iffalse ⊢ ( ¬ 𝜓 → if ( 𝜓 , 𝐴 , 𝐷 ) = 𝐷 )
10 iffalse ⊢ ( ¬ 𝜓 → if ( 𝜓 , 𝐶 , 𝐷 ) = 𝐷 )
11 9 10 eqtr4d ⊢ ( ¬ 𝜓 → if ( 𝜓 , 𝐴 , 𝐷 ) = if ( 𝜓 , 𝐶 , 𝐷 ) )
12 8 11 sylan9eq ⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → if ( 𝜓 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐶 , 𝐷 ) )
13 7 12 pm2.61dan ⊢ ( 𝜑 → if ( 𝜓 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐶 , 𝐷 ) )