Metamath Proof Explorer


Theorem outsideofcom

Description: Commutativity law for outsideness. Theorem 6.6 of Schwabhauser p. 44. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion outsideofcom NP𝔼NA𝔼NB𝔼NPOutsideOfABPOutsideOfBA

Proof

Step Hyp Ref Expression
1 3ancoma APBPABtwnPBBBtwnPABPAPABtwnPBBBtwnPA
2 orcom ABtwnPBBBtwnPABBtwnPAABtwnPB
3 2 3anbi3i BPAPABtwnPBBBtwnPABPAPBBtwnPAABtwnPB
4 1 3 bitri APBPABtwnPBBBtwnPABPAPBBtwnPAABtwnPB
5 4 a1i NP𝔼NA𝔼NB𝔼NAPBPABtwnPBBBtwnPABPAPBBtwnPAABtwnPB
6 broutsideof2 NP𝔼NA𝔼NB𝔼NPOutsideOfABAPBPABtwnPBBBtwnPA
7 3ancomb P𝔼NA𝔼NB𝔼NP𝔼NB𝔼NA𝔼N
8 broutsideof2 NP𝔼NB𝔼NA𝔼NPOutsideOfBABPAPBBtwnPAABtwnPB
9 7 8 sylan2b NP𝔼NA𝔼NB𝔼NPOutsideOfBABPAPBBtwnPAABtwnPB
10 5 6 9 3bitr4d NP𝔼NA𝔼NB𝔼NPOutsideOfABPOutsideOfBA