Theorem problem3

Description: Practice problem 3. Clues: eqcomi eqtri subaddrii recni 4re 3re 1re df-4 addcomi . (Contributed by Filip Cernatescu, 16-Mar-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	problem3.1	$$⊢A\in ℂ$$
	problem3.2	$$⊢A+3=4$$
Assertion	problem3	$$⊢A=1$$

Proof

Step	Hyp	Ref	Expression
1		problem3.1	$$⊢A\in ℂ$$
2		problem3.2	$$⊢A+3=4$$
3		4re	$$⊢4\in ℝ$$
4	3	recni	$$⊢4\in ℂ$$
5		3re	$$⊢3\in ℝ$$
6	5	recni	$$⊢3\in ℂ$$
7		1re	$$⊢1\in ℝ$$
8	7	recni	$$⊢1\in ℂ$$
9		df-4	$$⊢4=3+1$$
10	9	eqcomi	$$⊢3+1=4$$
11	4 6 8 10	subaddrii	$$⊢4-3=1$$
12	11	eqcomi	$$⊢1=4-3$$
13	6 1	addcomi	$$⊢3+A=A+3$$
14	13 2	eqtri	$$⊢3+A=4$$
15	4 6 1 14	subaddrii	$$⊢4-3=A$$
16	12 15	eqtri	$$⊢1=A$$
17	16	eqcomi	$$⊢A=1$$