Step |
Hyp |
Ref |
Expression |
1 |
|
pm3.13 |
⊢ ( ¬ ( 𝜑 ∧ 𝜓 ) → ( ¬ 𝜑 ∨ ¬ 𝜓 ) ) |
2 |
|
iffalse |
⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = if ( 𝜓 , 𝐵 , 𝐶 ) ) |
3 |
|
iffalse |
⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 𝐶 ) = 𝐶 ) |
4 |
3
|
ifeq2d |
⊢ ( ¬ 𝜑 → if ( 𝜓 , 𝐵 , if ( 𝜑 , 𝐴 , 𝐶 ) ) = if ( 𝜓 , 𝐵 , 𝐶 ) ) |
5 |
2 4
|
eqtr4d |
⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = if ( 𝜓 , 𝐵 , if ( 𝜑 , 𝐴 , 𝐶 ) ) ) |
6 |
|
iffalse |
⊢ ( ¬ 𝜓 → if ( 𝜓 , 𝐵 , 𝐶 ) = 𝐶 ) |
7 |
6
|
ifeq2d |
⊢ ( ¬ 𝜓 → if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = if ( 𝜑 , 𝐴 , 𝐶 ) ) |
8 |
|
iffalse |
⊢ ( ¬ 𝜓 → if ( 𝜓 , 𝐵 , if ( 𝜑 , 𝐴 , 𝐶 ) ) = if ( 𝜑 , 𝐴 , 𝐶 ) ) |
9 |
7 8
|
eqtr4d |
⊢ ( ¬ 𝜓 → if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = if ( 𝜓 , 𝐵 , if ( 𝜑 , 𝐴 , 𝐶 ) ) ) |
10 |
5 9
|
jaoi |
⊢ ( ( ¬ 𝜑 ∨ ¬ 𝜓 ) → if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = if ( 𝜓 , 𝐵 , if ( 𝜑 , 𝐴 , 𝐶 ) ) ) |
11 |
1 10
|
syl |
⊢ ( ¬ ( 𝜑 ∧ 𝜓 ) → if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = if ( 𝜓 , 𝐵 , if ( 𝜑 , 𝐴 , 𝐶 ) ) ) |