Metamath Proof Explorer

Theorem sadadd2lem2

Description: The core of the proof of sadadd2 . The intuitive justification for this is that cadd is true if at least two arguments are true, and hadd is true if an odd number of arguments are true, so altogether the result is n x. A where n is the number of true arguments, which is equivalently obtained by adding together one A for each true argument, on the right side. (Contributed by Mario Carneiro, 8-Sep-2016)

Ref Expression
Assertion sadadd2lem2 ( 𝐴 ∈ ℂ → ( if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) + if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + if ( 𝜒 , 𝐴 , 0 ) ) )

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 ifcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝜓 , 𝐴 , 0 ) ∈ ℂ )
3 1 2 mpan2 ⊢ ( 𝐴 ∈ ℂ → if ( 𝜓 , 𝐴 , 0 ) ∈ ℂ )
4 3 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → if ( 𝜓 , 𝐴 , 0 ) ∈ ℂ )
5 simpll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → 𝐴 ∈ ℂ )
6 4 5 5 add12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( if ( 𝜓 , 𝐴 , 0 ) + ( 𝐴 + 𝐴 ) ) = ( 𝐴 + ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) ) )
7 5 4 5 addassd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) = ( 𝐴 + ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) ) )
8 6 7 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( if ( 𝜓 , 𝐴 , 0 ) + ( 𝐴 + 𝐴 ) ) = ( ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) )
9 pm5.501 ⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜑 ↔ 𝜓 ) ) )
10 9 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( 𝜓 ↔ ( 𝜑 ↔ 𝜓 ) ) )
11 10 bicomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( ( 𝜑 ↔ 𝜓 ) ↔ 𝜓 ) )
12 11 ifbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) = if ( 𝜓 , 𝐴 , 0 ) )
13 animorrl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( 𝜑 ∨ 𝜓 ) )
14 iftrue ⊢ ( ( 𝜑 ∨ 𝜓 ) → if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) = ( 2 · 𝐴 ) )
15 13 14 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) = ( 2 · 𝐴 ) )
16 5 2timesd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
17 15 16 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) = ( 𝐴 + 𝐴 ) )
18 12 17 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + ( 𝐴 + 𝐴 ) ) )
19 iftrue ⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 0 ) = 𝐴 )
20 19 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → if ( 𝜑 , 𝐴 , 0 ) = 𝐴 )
21 20 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) )
22 21 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) = ( ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) )
23 8 18 22 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) )
24 iffalse ⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 0 ) = 0 )
25 24 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜑 , 𝐴 , 0 ) = 0 )
26 25 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 0 + if ( 𝜓 , 𝐴 , 0 ) ) )
27 3 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜓 , 𝐴 , 0 ) ∈ ℂ )
28 27 addlidd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( 0 + if ( 𝜓 , 𝐴 , 0 ) ) = if ( 𝜓 , 𝐴 , 0 ) )
29 26 28 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = if ( 𝜓 , 𝐴 , 0 ) )
30 29 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) = ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) )
31 2cnd ⊢ ( 𝐴 ∈ ℂ → 2 ∈ ℂ )
32 id ⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
33 31 32 mulcld ⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) ∈ ℂ )
34 33 addlidd ⊢ ( 𝐴 ∈ ℂ → ( 0 + ( 2 · 𝐴 ) ) = ( 2 · 𝐴 ) )
35 2times ⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
36 34 35 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( 0 + ( 2 · 𝐴 ) ) = ( 𝐴 + 𝐴 ) )
37 36 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( 0 + ( 2 · 𝐴 ) ) = ( 𝐴 + 𝐴 ) )
38 iftrue ⊢ ( 𝜓 → if ( 𝜓 , 0 , 𝐴 ) = 0 )
39 38 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → if ( 𝜓 , 0 , 𝐴 ) = 0 )
40 iftrue ⊢ ( 𝜓 → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = ( 2 · 𝐴 ) )
41 40 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = ( 2 · 𝐴 ) )
42 39 41 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( 0 + ( 2 · 𝐴 ) ) )
43 iftrue ⊢ ( 𝜓 → if ( 𝜓 , 𝐴 , 0 ) = 𝐴 )
44 43 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → if ( 𝜓 , 𝐴 , 0 ) = 𝐴 )
45 44 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) = ( 𝐴 + 𝐴 ) )
46 37 42 45 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) )
47 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → 𝐴 ∈ ℂ )
48 0cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → 0 ∈ ℂ )
49 47 48 addcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → ( 𝐴 + 0 ) = ( 0 + 𝐴 ) )
50 iffalse ⊢ ( ¬ 𝜓 → if ( 𝜓 , 0 , 𝐴 ) = 𝐴 )
51 50 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → if ( 𝜓 , 0 , 𝐴 ) = 𝐴 )
52 iffalse ⊢ ( ¬ 𝜓 → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = 0 )
53 52 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = 0 )
54 51 53 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( 𝐴 + 0 ) )
55 iffalse ⊢ ( ¬ 𝜓 → if ( 𝜓 , 𝐴 , 0 ) = 0 )
56 55 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → if ( 𝜓 , 𝐴 , 0 ) = 0 )
57 56 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) = ( 0 + 𝐴 ) )
58 49 54 57 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) )
59 46 58 pm2.61dan ⊢ ( 𝐴 ∈ ℂ → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) )
60 59 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) )
61 ifnot ⊢ if ( ¬ 𝜓 , 𝐴 , 0 ) = if ( 𝜓 , 0 , 𝐴 )
62 nbn2 ⊢ ( ¬ 𝜑 → ( ¬ 𝜓 ↔ ( 𝜑 ↔ 𝜓 ) ) )
63 62 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( ¬ 𝜓 ↔ ( 𝜑 ↔ 𝜓 ) ) )
64 63 ifbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → if ( ¬ 𝜓 , 𝐴 , 0 ) = if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) )
65 61 64 eqtr3id ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜓 , 0 , 𝐴 ) = if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) )
66 biorf ⊢ ( ¬ 𝜑 → ( 𝜓 ↔ ( 𝜑 ∨ 𝜓 ) ) )
67 66 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( 𝜓 ↔ ( 𝜑 ∨ 𝜓 ) ) )
68 67 ifbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) )
69 65 68 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) )
70 30 60 69 3eqtr2rd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) )
71 23 70 pm2.61dan ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → ( if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) )
72 hadrot ⊢ ( hadd ( 𝜒 , 𝜑 , 𝜓 ) ↔ hadd ( 𝜑 , 𝜓 , 𝜒 ) )
73 had1 ⊢ ( 𝜒 → ( hadd ( 𝜒 , 𝜑 , 𝜓 ) ↔ ( 𝜑 ↔ 𝜓 ) ) )
74 72 73 bitr3id ⊢ ( 𝜒 → ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑 ↔ 𝜓 ) ) )
75 74 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑 ↔ 𝜓 ) ) )
76 75 ifbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) = if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) )
77 cad1 ⊢ ( 𝜒 → ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑 ∨ 𝜓 ) ) )
78 77 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑 ∨ 𝜓 ) ) )
79 78 ifbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) = if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) )
80 76 79 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → ( if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) + if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) )
81 iftrue ⊢ ( 𝜒 → if ( 𝜒 , 𝐴 , 0 ) = 𝐴 )
82 81 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → if ( 𝜒 , 𝐴 , 0 ) = 𝐴 )
83 82 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + if ( 𝜒 , 𝐴 , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) )
84 71 80 83 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → ( if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) + if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + if ( 𝜒 , 𝐴 , 0 ) ) )
85 19 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → if ( 𝜑 , 𝐴 , 0 ) = 𝐴 )
86 85 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) )
87 44 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) = ( 𝐴 + 𝐴 ) )
88 37 42 87 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) )
89 53 56 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = if ( 𝜓 , 𝐴 , 0 ) )
90 51 89 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) )
91 88 90 pm2.61dan ⊢ ( 𝐴 ∈ ℂ → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) )
92 91 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) )
93 9 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( 𝜓 ↔ ( 𝜑 ↔ 𝜓 ) ) )
94 93 notbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( ¬ 𝜓 ↔ ¬ ( 𝜑 ↔ 𝜓 ) ) )
95 df-xor ⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ ¬ ( 𝜑 ↔ 𝜓 ) )
96 94 95 bitr4di ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( ¬ 𝜓 ↔ ( 𝜑 ⊻ 𝜓 ) ) )
97 96 ifbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → if ( ¬ 𝜓 , 𝐴 , 0 ) = if ( ( 𝜑 ⊻ 𝜓 ) , 𝐴 , 0 ) )
98 61 97 eqtr3id ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → if ( 𝜓 , 0 , 𝐴 ) = if ( ( 𝜑 ⊻ 𝜓 ) , 𝐴 , 0 ) )
99 ibar ⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜑 ∧ 𝜓 ) ) )
100 99 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( 𝜓 ↔ ( 𝜑 ∧ 𝜓 ) ) )
101 100 ifbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = if ( ( 𝜑 ∧ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) )
102 98 101 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( ( 𝜑 ⊻ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∧ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) )
103 86 92 102 3eqtr2rd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( if ( ( 𝜑 ⊻ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∧ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
104 simplll ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) ∧ 𝜓 ) → 𝐴 ∈ ℂ )
105 0cnd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) ∧ ¬ 𝜓 ) → 0 ∈ ℂ )
106 104 105 ifclda ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜓 , 𝐴 , 0 ) ∈ ℂ )
107 0cnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → 0 ∈ ℂ )
108 106 107 addcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜓 , 𝐴 , 0 ) + 0 ) = ( 0 + if ( 𝜓 , 𝐴 , 0 ) ) )
109 62 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( ¬ 𝜓 ↔ ( 𝜑 ↔ 𝜓 ) ) )
110 109 con1bid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ 𝜓 ) )
111 95 110 bitrid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( ( 𝜑 ⊻ 𝜓 ) ↔ 𝜓 ) )
112 111 ifbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → if ( ( 𝜑 ⊻ 𝜓 ) , 𝐴 , 0 ) = if ( 𝜓 , 𝐴 , 0 ) )
113 simpr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ¬ 𝜑 )
114 113 intnanrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ¬ ( 𝜑 ∧ 𝜓 ) )
115 iffalse ⊢ ( ¬ ( 𝜑 ∧ 𝜓 ) → if ( ( 𝜑 ∧ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) = 0 )
116 114 115 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → if ( ( 𝜑 ∧ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) = 0 )
117 112 116 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( ( 𝜑 ⊻ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∧ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + 0 ) )
118 24 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜑 , 𝐴 , 0 ) = 0 )
119 118 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 0 + if ( 𝜓 , 𝐴 , 0 ) ) )
120 108 117 119 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( ( 𝜑 ⊻ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∧ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
121 103 120 pm2.61dan ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → ( if ( ( 𝜑 ⊻ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∧ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
122 had0 ⊢ ( ¬ 𝜒 → ( hadd ( 𝜒 , 𝜑 , 𝜓 ) ↔ ( 𝜑 ⊻ 𝜓 ) ) )
123 72 122 bitr3id ⊢ ( ¬ 𝜒 → ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑 ⊻ 𝜓 ) ) )
124 123 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑 ⊻ 𝜓 ) ) )
125 124 ifbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) = if ( ( 𝜑 ⊻ 𝜓 ) , 𝐴 , 0 ) )
126 cad0 ⊢ ( ¬ 𝜒 → ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑 ∧ 𝜓 ) ) )
127 126 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑 ∧ 𝜓 ) ) )
128 127 ifbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) = if ( ( 𝜑 ∧ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) )
129 125 128 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → ( if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) + if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( ( 𝜑 ⊻ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∧ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) )
130 iffalse ⊢ ( ¬ 𝜒 → if ( 𝜒 , 𝐴 , 0 ) = 0 )
131 130 oveq2d ⊢ ( ¬ 𝜒 → ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + if ( 𝜒 , 𝐴 , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 0 ) )
132 ifcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝜑 , 𝐴 , 0 ) ∈ ℂ )
133 1 132 mpan2 ⊢ ( 𝐴 ∈ ℂ → if ( 𝜑 , 𝐴 , 0 ) ∈ ℂ )
134 133 3 addcld ⊢ ( 𝐴 ∈ ℂ → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) ∈ ℂ )
135 134 addridd ⊢ ( 𝐴 ∈ ℂ → ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 0 ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
136 131 135 sylan9eqr ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + if ( 𝜒 , 𝐴 , 0 ) ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
137 121 129 136 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → ( if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) + if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + if ( 𝜒 , 𝐴 , 0 ) ) )
138 84 137 pm2.61dan ⊢ ( 𝐴 ∈ ℂ → ( if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) + if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + if ( 𝜒 , 𝐴 , 0 ) ) )