![]() |
Mathbox for Scott Fenton |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > btwncom | Structured version Visualization version GIF version |
Description: Betweenness commutes. (Contributed by Scott Fenton, 12-Jun-2013.) |
Ref | Expression |
---|---|
btwncom | ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Btwn 〈𝐵, 𝐶〉 ↔ 𝐴 Btwn 〈𝐶, 𝐵〉)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | btwncomim 32625 | . 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Btwn 〈𝐵, 𝐶〉 → 𝐴 Btwn 〈𝐶, 𝐵〉)) | |
2 | 3ancomb 1122 | . . 3 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ↔ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) | |
3 | btwncomim 32625 | . . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝐴 Btwn 〈𝐶, 𝐵〉 → 𝐴 Btwn 〈𝐵, 𝐶〉)) | |
4 | 2, 3 | sylan2b 588 | . 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Btwn 〈𝐶, 𝐵〉 → 𝐴 Btwn 〈𝐵, 𝐶〉)) |
5 | 1, 4 | impbid 204 | 1 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Btwn 〈𝐵, 𝐶〉 ↔ 𝐴 Btwn 〈𝐶, 𝐵〉)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 385 ∧ w3a 1108 ∈ wcel 2157 〈cop 4372 class class class wbr 4841 ‘cfv 6099 ℕcn 11310 𝔼cee 26117 Btwn cbtwn 26118 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 ax-rep 4962 ax-sep 4973 ax-nul 4981 ax-pow 5033 ax-pr 5095 ax-un 7181 ax-inf2 8786 ax-cnex 10278 ax-resscn 10279 ax-1cn 10280 ax-icn 10281 ax-addcl 10282 ax-addrcl 10283 ax-mulcl 10284 ax-mulrcl 10285 ax-mulcom 10286 ax-addass 10287 ax-mulass 10288 ax-distr 10289 ax-i2m1 10290 ax-1ne0 10291 ax-1rid 10292 ax-rnegex 10293 ax-rrecex 10294 ax-cnre 10295 ax-pre-lttri 10296 ax-pre-lttrn 10297 ax-pre-ltadd 10298 ax-pre-mulgt0 10299 ax-pre-sup 10300 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-fal 1667 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2590 df-eu 2607 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ne 2970 df-nel 3073 df-ral 3092 df-rex 3093 df-reu 3094 df-rmo 3095 df-rab 3096 df-v 3385 df-sbc 3632 df-csb 3727 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-pss 3783 df-nul 4114 df-if 4276 df-pw 4349 df-sn 4367 df-pr 4369 df-tp 4371 df-op 4373 df-uni 4627 df-int 4666 df-iun 4710 df-br 4842 df-opab 4904 df-mpt 4921 df-tr 4944 df-id 5218 df-eprel 5223 df-po 5231 df-so 5232 df-fr 5269 df-se 5270 df-we 5271 df-xp 5316 df-rel 5317 df-cnv 5318 df-co 5319 df-dm 5320 df-rn 5321 df-res 5322 df-ima 5323 df-pred 5896 df-ord 5942 df-on 5943 df-lim 5944 df-suc 5945 df-iota 6062 df-fun 6101 df-fn 6102 df-f 6103 df-f1 6104 df-fo 6105 df-f1o 6106 df-fv 6107 df-isom 6108 df-riota 6837 df-ov 6879 df-oprab 6880 df-mpt2 6881 df-om 7298 df-1st 7399 df-2nd 7400 df-wrecs 7643 df-recs 7705 df-rdg 7743 df-1o 7797 df-oadd 7801 df-er 7980 df-map 8095 df-en 8194 df-dom 8195 df-sdom 8196 df-fin 8197 df-sup 8588 df-oi 8655 df-card 9049 df-pnf 10363 df-mnf 10364 df-xr 10365 df-ltxr 10366 df-le 10367 df-sub 10556 df-neg 10557 df-div 10975 df-nn 11311 df-2 11372 df-3 11373 df-n0 11577 df-z 11663 df-uz 11927 df-rp 12071 df-ico 12426 df-icc 12427 df-fz 12577 df-fzo 12717 df-seq 13052 df-exp 13111 df-hash 13367 df-cj 14177 df-re 14178 df-im 14179 df-sqrt 14313 df-abs 14314 df-clim 14557 df-sum 14755 df-ee 26120 df-btwn 26121 df-cgr 26122 |
This theorem is referenced by: btwncomand 32627 btwntriv1 32628 btwnswapid2 32630 btwnintr 32631 btwnexch3 32632 btwnouttr 32636 btwnexch 32637 trisegint 32640 ifscgr 32656 colinearperm1 32674 lineext 32688 fscgr 32692 btwnconn1lem13 32711 colinbtwnle 32730 broutsideof2 32734 lineunray 32759 |
Copyright terms: Public domain | W3C validator |