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 13 iftrued ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) = ( 2 · 𝐴 ) )
15 5 2timesd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
16 14 15 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) = ( 𝐴 + 𝐴 ) )
17 12 16 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + ( 𝐴 + 𝐴 ) ) )
18 iftrue ⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 0 ) = 𝐴 )
19 18 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → if ( 𝜑 , 𝐴 , 0 ) = 𝐴 )
20 19 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) )
21 20 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) = ( ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) )
22 8 17 21 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) )
23 iffalse ⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 0 ) = 0 )
24 23 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜑 , 𝐴 , 0 ) = 0 )
25 24 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 0 + if ( 𝜓 , 𝐴 , 0 ) ) )
26 3 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜓 , 𝐴 , 0 ) ∈ ℂ )
27 26 addlidd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( 0 + if ( 𝜓 , 𝐴 , 0 ) ) = if ( 𝜓 , 𝐴 , 0 ) )
28 25 27 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = if ( 𝜓 , 𝐴 , 0 ) )
29 28 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) = ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) )
30 2cnd ⊢ ( 𝐴 ∈ ℂ → 2 ∈ ℂ )
31 id ⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
32 30 31 mulcld ⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) ∈ ℂ )
33 32 addlidd ⊢ ( 𝐴 ∈ ℂ → ( 0 + ( 2 · 𝐴 ) ) = ( 2 · 𝐴 ) )
34 2times ⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
35 33 34 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( 0 + ( 2 · 𝐴 ) ) = ( 𝐴 + 𝐴 ) )
36 35 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( 0 + ( 2 · 𝐴 ) ) = ( 𝐴 + 𝐴 ) )
37 iftrue ⊢ ( 𝜓 → if ( 𝜓 , 0 , 𝐴 ) = 0 )
38 37 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → if ( 𝜓 , 0 , 𝐴 ) = 0 )
39 iftrue ⊢ ( 𝜓 → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = ( 2 · 𝐴 ) )
40 39 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = ( 2 · 𝐴 ) )
41 38 40 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( 0 + ( 2 · 𝐴 ) ) )
42 iftrue ⊢ ( 𝜓 → if ( 𝜓 , 𝐴 , 0 ) = 𝐴 )
43 42 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → if ( 𝜓 , 𝐴 , 0 ) = 𝐴 )
44 43 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) = ( 𝐴 + 𝐴 ) )
45 36 41 44 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) )
46 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → 𝐴 ∈ ℂ )
47 0cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → 0 ∈ ℂ )
48 46 47 addcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → ( 𝐴 + 0 ) = ( 0 + 𝐴 ) )
49 iffalse ⊢ ( ¬ 𝜓 → if ( 𝜓 , 0 , 𝐴 ) = 𝐴 )
50 49 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → if ( 𝜓 , 0 , 𝐴 ) = 𝐴 )
51 iffalse ⊢ ( ¬ 𝜓 → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = 0 )
52 51 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = 0 )
53 50 52 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( 𝐴 + 0 ) )
54 iffalse ⊢ ( ¬ 𝜓 → if ( 𝜓 , 𝐴 , 0 ) = 0 )
55 54 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → if ( 𝜓 , 𝐴 , 0 ) = 0 )
56 55 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) = ( 0 + 𝐴 ) )
57 48 53 56 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) )
58 45 57 pm2.61dan ⊢ ( 𝐴 ∈ ℂ → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) )
59 58 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) )
60 ifnot ⊢ if ( ¬ 𝜓 , 𝐴 , 0 ) = if ( 𝜓 , 0 , 𝐴 )
61 nbn2 ⊢ ( ¬ 𝜑 → ( ¬ 𝜓 ↔ ( 𝜑 ↔ 𝜓 ) ) )
62 61 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( ¬ 𝜓 ↔ ( 𝜑 ↔ 𝜓 ) ) )
63 62 ifbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → if ( ¬ 𝜓 , 𝐴 , 0 ) = if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) )
64 60 63 eqtr3id ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜓 , 0 , 𝐴 ) = if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) )
65 biorf ⊢ ( ¬ 𝜑 → ( 𝜓 ↔ ( 𝜑 ∨ 𝜓 ) ) )
66 65 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( 𝜓 ↔ ( 𝜑 ∨ 𝜓 ) ) )
67 66 ifbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) )
68 64 67 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) )
69 29 59 68 3eqtr2rd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) )
70 22 69 pm2.61dan ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → ( if ( ( 𝜑 ↔ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∨ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) )
71 hadrot ⊢ ( hadd ( 𝜒 , 𝜑 , 𝜓 ) ↔ hadd ( 𝜑 , 𝜓 , 𝜒 ) )
72 had1 ⊢ ( 𝜒 ↔ ( hadd ( 𝜒 , 𝜑 , 𝜓 ) ↔ ( 𝜑 ↔ 𝜓 ) ) )
73 72 biimpi ⊢ ( 𝜒 → ( hadd ( 𝜒 , 𝜑 , 𝜓 ) ↔ ( 𝜑 ↔ 𝜓 ) ) )
74 71 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 70 80 83 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → ( if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) + if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + if ( 𝜒 , 𝐴 , 0 ) ) )
85 18 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → if ( 𝜑 , 𝐴 , 0 ) = 𝐴 )
86 85 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) )
87 43 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) = ( 𝐴 + 𝐴 ) )
88 36 41 87 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) )
89 52 55 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = if ( 𝜓 , 𝐴 , 0 ) )
90 50 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 60 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 61 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( ¬ 𝜓 ↔ ( 𝜑 ↔ 𝜓 ) ) )
110 109 con1bid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ 𝜓 ) )
111 95 110 bitrid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( ( 𝜑 ⊻ 𝜓 ) ↔ 𝜓 ) )
112 111 ifbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → if ( ( 𝜑 ⊻ 𝜓 ) , 𝐴 , 0 ) = if ( 𝜓 , 𝐴 , 0 ) )
113 simpr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ¬ 𝜑 )
114 113 intnanrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ¬ ( 𝜑 ∧ 𝜓 ) )
115 114 iffalsed ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → if ( ( 𝜑 ∧ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) = 0 )
116 112 115 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( ( 𝜑 ⊻ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∧ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + 0 ) )
117 23 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜑 , 𝐴 , 0 ) = 0 )
118 117 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 0 + if ( 𝜓 , 𝐴 , 0 ) ) )
119 108 116 118 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( ( 𝜑 ⊻ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∧ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
120 103 119 pm2.61dan ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → ( if ( ( 𝜑 ⊻ 𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑 ∧ 𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
121 had0 ⊢ ( ¬ 𝜒 ↔ ( hadd ( 𝜒 , 𝜑 , 𝜓 ) ↔ ( 𝜑 ⊻ 𝜓 ) ) )
122 121 biimpi ⊢ ( ¬ 𝜒 → ( hadd ( 𝜒 , 𝜑 , 𝜓 ) ↔ ( 𝜑 ⊻ 𝜓 ) ) )
123 71 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 120 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 ) ) )