Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  4atex Structured version   Unicode version

Theorem 4atex 33560
 Description: Whenever there are at least 4 atoms under (specifically, , , , and ), there are also at least 4 atoms under . This proves the statement in Lemma E of [Crawley] p. 114, last line, "...p q/0 and hence p s/0 contains at least four atoms..." Note that by cvlsupr2 32828, our is a shorter way to express . (Contributed by NM, 27-May-2013.)
Hypotheses
Ref Expression
4that.l
4that.j
4that.a
4that.h
Assertion
Ref Expression
4atex
Distinct variable groups:   ,,   ,   ,,   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hint:   ()

Proof of Theorem 4atex
StepHypRef Expression
1 simp21l 1122 . . . . 5
21ad2antrr 730 . . . 4
3 simp21r 1123 . . . . 5
43ad2antrr 730 . . . 4
5 oveq1 6309 . . . . . 6
65eqcoms 2434 . . . . 5
76adantl 467 . . . 4
8 breq1 4423 . . . . . . 7
98notbid 295 . . . . . 6
10 oveq2 6310 . . . . . . 7
11 oveq2 6310 . . . . . . 7
1210, 11eqeq12d 2444 . . . . . 6
139, 12anbi12d 715 . . . . 5
1413rspcev 3182 . . . 4
152, 4, 7, 14syl12anc 1262 . . 3
16 simpl3r 1061 . . . . . 6
1716ad2antrr 730 . . . . 5
18 oveq1 6309 . . . . . . . . . 10
1918eqeq2d 2436 . . . . . . . . 9
2019anbi2d 708 . . . . . . . 8
2120rexbidv 2939 . . . . . . 7
22 breq1 4423 . . . . . . . . . 10
2322notbid 295 . . . . . . . . 9
24 oveq2 6310 . . . . . . . . . 10
25 oveq2 6310 . . . . . . . . . 10
2624, 25eqeq12d 2444 . . . . . . . . 9
2723, 26anbi12d 715 . . . . . . . 8
2827cbvrexv 3056 . . . . . . 7
2921, 28syl6rbbr 267 . . . . . 6
3029adantl 467 . . . . 5
3117, 30mpbid 213 . . . 4
32 simp22l 1124 . . . . . 6
3332ad3antrrr 734 . . . . 5
34 simp22r 1125 . . . . . 6
3534ad3antrrr 734 . . . . 5
36 simp3l 1033 . . . . . . . 8
3736necomd 2695 . . . . . . 7
3837ad3antrrr 734 . . . . . 6
39 simpr 462 . . . . . . 7
4039necomd 2695 . . . . . 6
41 simpllr 767 . . . . . . 7
42 simp1l 1029 . . . . . . . . . 10
43 hlcvl 32844 . . . . . . . . . 10
4442, 43syl 17 . . . . . . . . 9
4544ad3antrrr 734 . . . . . . . 8
46 simp23 1040 . . . . . . . . 9
4746ad3antrrr 734 . . . . . . . 8
481ad3antrrr 734 . . . . . . . 8
49 simplr 760 . . . . . . . 8
50 4that.l . . . . . . . . 9
51 4that.j . . . . . . . . 9
52 4that.a . . . . . . . . 9
5350, 51, 52cvlatexch1 32821 . . . . . . . 8
5445, 47, 33, 48, 49, 53syl131anc 1277 . . . . . . 7
5541, 54mpd 15 . . . . . 6
5649necomd 2695 . . . . . . 7
5752, 50, 51cvlsupr2 32828 . . . . . . 7
5845, 48, 47, 33, 56, 57syl131anc 1277 . . . . . 6
5938, 40, 55, 58mpbir3and 1188 . . . . 5
60 breq1 4423 . . . . . . . 8
6160notbid 295 . . . . . . 7
62 oveq2 6310 . . . . . . . 8
63 oveq2 6310 . . . . . . . 8
6462, 63eqeq12d 2444 . . . . . . 7
6561, 64anbi12d 715 . . . . . 6
6665rspcev 3182 . . . . 5
6733, 35, 59, 66syl12anc 1262 . . . 4
6831, 67pm2.61dane 2742 . . 3
6915, 68pm2.61dane 2742 . 2
70 simpl1 1008 . . 3
71 simpl2 1009 . . 3
72 simpl3l 1060 . . 3
73 simpr 462 . . 3
74 simpl3r 1061 . . 3
75 4that.h . . . 4
7650, 51, 52, 754atexlem7 33559 . . 3
7770, 71, 72, 73, 74, 76syl113anc 1276 . 2
7869, 77pm2.61dan 798 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370   w3a 982   wceq 1437   wcel 1868   wne 2618  wrex 2776   class class class wbr 4420  cfv 5598  (class class class)co 6302  cple 15185  cjn 16177  catm 32748  clc 32750  chlt 32835  clh 33468 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-riota 6264  df-ov 6305  df-oprab 6306  df-preset 16161  df-poset 16179  df-plt 16192  df-lub 16208  df-glb 16209  df-join 16210  df-meet 16211  df-p0 16273  df-p1 16274  df-lat 16280  df-clat 16342  df-oposet 32661  df-ol 32663  df-oml 32664  df-covers 32751  df-ats 32752  df-atl 32783  df-cvlat 32807  df-hlat 32836  df-llines 32982  df-lplanes 32983  df-lhyp 33472 This theorem is referenced by:  4atex2  33561
 Copyright terms: Public domain W3C validator