Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  5oalem6 Structured version   Unicode version

Theorem 5oalem6 27147
 Description: Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000.) (New usage is discouraged.)
Hypotheses
Ref Expression
5oalem5.1
5oalem5.2
5oalem5.3
5oalem5.4
5oalem5.5
5oalem5.6
5oalem5.7
5oalem5.8
Assertion
Ref Expression
5oalem6

Proof of Theorem 5oalem6
StepHypRef Expression
1 an4 831 . . . 4
2 an4 831 . . . 4
3 eqeq1 2433 . . . . . . . . . . 11
43biimpcd 227 . . . . . . . . . 10
5 eqeq1 2433 . . . . . . . . . . 11
65biimpcd 227 . . . . . . . . . 10
74, 6anim12d 565 . . . . . . . . 9
8 eqeq1 2433 . . . . . . . . . 10
98biimpcd 227 . . . . . . . . 9
107, 9anim12d 565 . . . . . . . 8
1110expdcom 440 . . . . . . 7
1211imp32 434 . . . . . 6
1312anim2i 571 . . . . 5
1413an4s 833 . . . 4
151, 2, 14syl2anb 481 . . 3
16 5oalem5.1 . . . 4
17 5oalem5.2 . . . 4
18 5oalem5.3 . . . 4
19 5oalem5.4 . . . 4
20 5oalem5.5 . . . 4
21 5oalem5.6 . . . 4
22 5oalem5.7 . . . 4
23 5oalem5.8 . . . 4
2416, 17, 18, 19, 20, 21, 22, 235oalem5 27146 . . 3
2515, 24syl 17 . 2
2616, 18shscli 26805 . . . . . . . . . 10
2717, 19shscli 26805 . . . . . . . . . 10
2826, 27shincli 26850 . . . . . . . . 9
2916, 22shscli 26805 . . . . . . . . . . 11
3017, 23shscli 26805 . . . . . . . . . . 11
3129, 30shincli 26850 . . . . . . . . . 10
3218, 22shscli 26805 . . . . . . . . . . 11
3319, 23shscli 26805 . . . . . . . . . . 11
3432, 33shincli 26850 . . . . . . . . . 10
3531, 34shscli 26805 . . . . . . . . 9
3628, 35shincli 26850 . . . . . . . 8
3716, 20shscli 26805 . . . . . . . . . . 11
3817, 21shscli 26805 . . . . . . . . . . 11
3937, 38shincli 26850 . . . . . . . . . 10
4020, 22shscli 26805 . . . . . . . . . . . 12
4121, 23shscli 26805 . . . . . . . . . . . 12
4240, 41shincli 26850 . . . . . . . . . . 11
4331, 42shscli 26805 . . . . . . . . . 10
4439, 43shincli 26850 . . . . . . . . 9
4518, 20shscli 26805 . . . . . . . . . . 11
4619, 21shscli 26805 . . . . . . . . . . 11
4745, 46shincli 26850 . . . . . . . . . 10
4834, 42shscli 26805 . . . . . . . . . 10
4947, 48shincli 26850 . . . . . . . . 9
5044, 49shscli 26805 . . . . . . . 8
5136, 50shincli 26850 . . . . . . 7
5216, 17, 18, 515oalem1 27142 . . . . . 6
5352expr 618 . . . . 5
5453adantrr 721 . . . 4