Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  addlocprlemeqgt Unicode version

 Description: Lemma for addlocpr 7363. This is a step used in both the and cases. (Contributed by Jim Kingdon, 7-Dec-2019.)
Hypotheses
Ref Expression
Assertion
Ref Expression

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
3 addlocprlem.a . . . . . 6
4 prop 7302 . . . . . 6
53, 4syl 14 . . . . 5
6 addlocprlem.uup . . . . 5
7 elprnqu 7309 . . . . 5
85, 6, 7syl2anc 408 . . . 4
9 addlocprlem.dlo . . . . . 6
10 elprnql 7308 . . . . . 6
115, 9, 10syl2anc 408 . . . . 5
12 addlocprlem.p . . . . 5
13 addclnq 7202 . . . . 5
1411, 12, 13syl2anc 408 . . . 4
15 addlocprlem.b . . . . . 6
16 prop 7302 . . . . . 6
1715, 16syl 14 . . . . 5
18 addlocprlem.tup . . . . 5
19 elprnqu 7309 . . . . 5
2017, 18, 19syl2anc 408 . . . 4
21 addlocprlem.elo . . . . . 6
22 elprnql 7308 . . . . . 6
2317, 21, 22syl2anc 408 . . . . 5
24 addclnq 7202 . . . . 5
2523, 12, 24syl2anc 408 . . . 4
26 lt2addnq 7231 . . . 4
278, 14, 20, 25, 26syl22anc 1217 . . 3
281, 2, 27mp2and 429 . 2
29 addcomnqg 7208 . . . 4