Step |
Hyp |
Ref |
Expression |
1 |
|
breq1 |
⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝐴 𝐶ℋ 𝐵 ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ 𝐵 ) ) |
2 |
|
fveq2 |
⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ⊥ ‘ 𝐴 ) = ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) ) |
3 |
2
|
breq1d |
⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐵 ↔ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) 𝐶ℋ 𝐵 ) ) |
4 |
1 3
|
bibi12d |
⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ( 𝐴 𝐶ℋ 𝐵 ↔ ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐵 ) ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ 𝐵 ↔ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) 𝐶ℋ 𝐵 ) ) ) |
5 |
|
breq2 |
⊢ ( 𝐵 = if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) → ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ 𝐵 ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) ) ) |
6 |
|
breq2 |
⊢ ( 𝐵 = if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) → ( ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) 𝐶ℋ 𝐵 ↔ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) 𝐶ℋ if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) ) ) |
7 |
5 6
|
bibi12d |
⊢ ( 𝐵 = if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) → ( ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ 𝐵 ↔ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) 𝐶ℋ 𝐵 ) ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) ↔ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) 𝐶ℋ if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) ) ) ) |
8 |
|
h0elch |
⊢ 0ℋ ∈ Cℋ |
9 |
8
|
elimel |
⊢ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∈ Cℋ |
10 |
8
|
elimel |
⊢ if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) ∈ Cℋ |
11 |
9 10
|
cmcm3i |
⊢ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) ↔ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) 𝐶ℋ if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) ) |
12 |
4 7 11
|
dedth2h |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝐵 ↔ ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐵 ) ) |