Theorem 2arwcatlem2

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

	Ref	Expression
Hypotheses	2arwcatlem2.a	$$⊢\phi \to A=X$$
	2arwcatlem2.b	$$⊢\phi \to B=Y$$
	2arwcatlem2.c	$$⊢\phi \to C=Z$$
	2arwcatlem2.f	$$⊢\phi \to \left(F=\underset{\dot{}}{0}\vee F=\underset{\dot{}}{1}\right)$$
	2arwcatlem2.1	$$⊢\phi \to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
	2arwcatlem2.0	$$⊢\phi \to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
Assertion	2arwcatlem2	$$⊢\phi \to \underset{\dot{}}{1}\left(⟨A,B⟩\underset{\dot{}}{·}C\right)F=F$$

Proof

Step	Hyp	Ref	Expression
1		2arwcatlem2.a	$$⊢\phi \to A=X$$
2		2arwcatlem2.b	$$⊢\phi \to B=Y$$
3		2arwcatlem2.c	$$⊢\phi \to C=Z$$
4		2arwcatlem2.f	$$⊢\phi \to \left(F=\underset{\dot{}}{0}\vee F=\underset{\dot{}}{1}\right)$$
5		2arwcatlem2.1	$$⊢\phi \to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
6		2arwcatlem2.0	$$⊢\phi \to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
7	1 2	opeq12d	$$⊢\phi \to ⟨A,B⟩=⟨X,Y⟩$$
8	7 3	oveq12d	$$⊢\phi \to ⟨A,B⟩\underset{\dot{}}{·}C=⟨X,Y⟩\underset{\dot{}}{·}Z$$
9	8	oveqd	$$⊢\phi \to \underset{\dot{}}{1}\left(⟨A,B⟩\underset{\dot{}}{·}C\right)F=\underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F$$
10	6	adantr	$$⊢\left(\phi \wedge F=\underset{\dot{}}{0}\right)\to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
11		simpr	$$⊢\left(\phi \wedge F=\underset{\dot{}}{0}\right)\to F=\underset{\dot{}}{0}$$
12	11	oveq2d	$$⊢\left(\phi \wedge F=\underset{\dot{}}{0}\right)\to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=\underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{0}$$
13	10 12 11	3eqtr4d	$$⊢\left(\phi \wedge F=\underset{\dot{}}{0}\right)\to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=F$$
14	5	adantr	$$⊢\left(\phi \wedge F=\underset{\dot{}}{1}\right)\to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
15		simpr	$$⊢\left(\phi \wedge F=\underset{\dot{}}{1}\right)\to F=\underset{\dot{}}{1}$$
16	15	oveq2d	$$⊢\left(\phi \wedge F=\underset{\dot{}}{1}\right)\to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=\underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{1}$$
17	14 16 15	3eqtr4d	$$⊢\left(\phi \wedge F=\underset{\dot{}}{1}\right)\to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=F$$
18	13 17 4	mpjaodan	$$⊢\phi \to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=F$$
19	9 18	eqtrd	$$⊢\phi \to \underset{\dot{}}{1}\left(⟨A,B⟩\underset{\dot{}}{·}C\right)F=F$$