Metamath Proof Explorer

Theorem ofscom

Description: The outer five segment predicate commutes. (Contributed by Scott Fenton, 26-Sep-2013)

Ref Expression
Assertion ofscom ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABCDOuterFiveSegEFGH↔EFGHOuterFiveSegABCD

Proof

Step Hyp Ref Expression
1 ancom ⊢BBtwnAC∧FBtwnEG↔FBtwnEG∧BBtwnAC
2 1 a1i ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→BBtwnAC∧FBtwnEG↔FBtwnEG∧BBtwnAC
3 simp11 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→N∈ℕ
4 simp12 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→A∈𝔼⁡N
5 simp13 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→B∈𝔼⁡N
6 simp23 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→E∈𝔼⁡N
7 simp31 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→F∈𝔼⁡N
8 cgrcom ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCgrEF↔EFCgrAB
9 3 4 5 6 7 8 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABCgrEF↔EFCgrAB
10 simp21 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→C∈𝔼⁡N
11 simp32 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→G∈𝔼⁡N
12 cgrcom ⊢N∈ℕ∧B∈𝔼⁡N∧C∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N→BCCgrFG↔FGCgrBC
13 3 5 10 7 11 12 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→BCCgrFG↔FGCgrBC
14 9 13 anbi12d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABCgrEF∧BCCgrFG↔EFCgrAB∧FGCgrBC
15 simp22 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→D∈𝔼⁡N
16 simp33 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→H∈𝔼⁡N
17 cgrcom ⊢N∈ℕ∧A∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧H∈𝔼⁡N→ADCgrEH↔EHCgrAD
18 3 4 15 6 16 17 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ADCgrEH↔EHCgrAD
19 cgrcom ⊢N∈ℕ∧B∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧H∈𝔼⁡N→BDCgrFH↔FHCgrBD
20 3 5 15 7 16 19 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→BDCgrFH↔FHCgrBD
21 18 20 anbi12d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ADCgrEH∧BDCgrFH↔EHCgrAD∧FHCgrBD
22 2 14 21 3anbi123d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→BBtwnAC∧FBtwnEG∧ABCgrEF∧BCCgrFG∧ADCgrEH∧BDCgrFH↔FBtwnEG∧BBtwnAC∧EFCgrAB∧FGCgrBC∧EHCgrAD∧FHCgrBD
23 brofs ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABCDOuterFiveSegEFGH↔BBtwnAC∧FBtwnEG∧ABCgrEF∧BCCgrFG∧ADCgrEH∧BDCgrFH
24 brofs ⊢N∈ℕ∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→EFGHOuterFiveSegABCD↔FBtwnEG∧BBtwnAC∧EFCgrAB∧FGCgrBC∧EHCgrAD∧FHCgrBD
25 3 6 7 11 16 4 5 10 15 24 syl333anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→EFGHOuterFiveSegABCD↔FBtwnEG∧BBtwnAC∧EFCgrAB∧FGCgrBC∧EHCgrAD∧FHCgrBD
26 22 23 25 3bitr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABCDOuterFiveSegEFGH↔EFGHOuterFiveSegABCD