Metamath Proof Explorer


Theorem cgrextendand

Description: Deduction form of cgrextend . (Contributed by Scott Fenton, 14-Oct-2013)

Ref Expression
Hypotheses cgrextendand.1 φ N
cgrextendand.2 φ A 𝔼 N
cgrextendand.3 φ B 𝔼 N
cgrextendand.4 φ C 𝔼 N
cgrextendand.5 φ D 𝔼 N
cgrextendand.6 φ E 𝔼 N
cgrextendand.7 φ F 𝔼 N
cgrextendand.8 φ ψ B Btwn A C
cgrextendand.9 φ ψ E Btwn D F
cgrextendand.10 φ ψ A B Cgr D E
cgrextendand.11 φ ψ B C Cgr E F
Assertion cgrextendand φ ψ A C Cgr D F

Proof

Step Hyp Ref Expression
1 cgrextendand.1 φ N
2 cgrextendand.2 φ A 𝔼 N
3 cgrextendand.3 φ B 𝔼 N
4 cgrextendand.4 φ C 𝔼 N
5 cgrextendand.5 φ D 𝔼 N
6 cgrextendand.6 φ E 𝔼 N
7 cgrextendand.7 φ F 𝔼 N
8 cgrextendand.8 φ ψ B Btwn A C
9 cgrextendand.9 φ ψ E Btwn D F
10 cgrextendand.10 φ ψ A B Cgr D E
11 cgrextendand.11 φ ψ B C Cgr E F
12 8 9 jca φ ψ B Btwn A C E Btwn D F
13 10 11 jca φ ψ A B Cgr D E B C Cgr E F
14 cgrextend N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N B Btwn A C E Btwn D F A B Cgr D E B C Cgr E F A C Cgr D F
15 1 2 3 4 5 6 7 14 syl133anc φ B Btwn A C E Btwn D F A B Cgr D E B C Cgr E F A C Cgr D F
16 15 adantr φ ψ B Btwn A C E Btwn D F A B Cgr D E B C Cgr E F A C Cgr D F
17 12 13 16 mp2and φ ψ A C Cgr D F