Theorem 2arwcatlem5

Description: Lemma for 2arwcat . (Contributed by Zhi Wang, 5-Nov-2025)

	Ref	Expression
Hypotheses	2arwcatlem5.1	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
	2arwcatlem5.2	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{0}$$
	2arwcatlem5.3	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
Assertion	2arwcatlem5	$$⊢\phi \to \left(\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\underset{\dot{}}{·}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		2arwcatlem5.1	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
2		2arwcatlem5.2	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{0}$$
3		2arwcatlem5.3	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
4		simpr	$$⊢\left(\phi \wedge \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
5	4	oveq1d	$$⊢\left(\phi \wedge \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}$$
6	4	oveq2d	$$⊢\left(\phi \wedge \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}$$
7	5 6	eqtr4d	$$⊢\left(\phi \wedge \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\underset{\dot{}}{·}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}\right)$$
8	1 2	eqtr4d	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{1}$$
9	8	adantr	$$⊢\left(\phi \wedge \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{1}\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{1}$$
10		simpr	$$⊢\left(\phi \wedge \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{1}\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{1}$$
11	10	oveq1d	$$⊢\left(\phi \wedge \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{1}\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{0}$$
12	10	oveq2d	$$⊢\left(\phi \wedge \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{1}\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{1}$$
13	9 11 12	3eqtr4d	$$⊢\left(\phi \wedge \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{1}\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\underset{\dot{}}{·}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}\right)$$
14		ovex	$$⊢\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}\in \mathrm{V}$$
15	14	elpr	$$⊢\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}\leftrightarrow \left(\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\vee \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{1}\right)$$
16	3 15	sylib	$$⊢\phi \to \left(\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\vee \underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{1}\right)$$
17	7 13 16	mpjaodan	$$⊢\phi \to \left(\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\underset{\dot{}}{·}\left(\underset{\dot{}}{0}\underset{\dot{}}{·}\underset{\dot{}}{0}\right)$$