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

Theorem cdlemefrs32fva 34038
 Description: Part of proof of Lemma E in [Crawley] p. 113. Value of at an atom not under . TODO: FIX COMMENT. TODO: consolidate uses of lhpmat 33666 here and elsewhere, and presence/absence of term. Also, why can proof be shortened with cdleme29cl 34015? What is difference from cdlemefs27cl 34051? (Contributed by NM, 29-Mar-2013.)
Hypotheses
Ref Expression
cdlemefrs27.b
cdlemefrs27.l
cdlemefrs27.j
cdlemefrs27.m
cdlemefrs27.a
cdlemefrs27.h
cdlemefrs27.eq
cdlemefrs27.nb
cdlemefrs27.rnb
cdleme29frs.o
Assertion
Ref Expression
cdlemefrs32fva
Distinct variable groups:   ,,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,,   ,   ,,   ,   ,   ,   ,   ,   ,,   ,
Allowed substitution hints:   (,)   ()   ()   ()   ()   ()   ()   (,,)

Proof of Theorem cdlemefrs32fva
StepHypRef Expression
1 simp2rl 1099 . . 3
2 cdlemefrs27.b . . . 4
3 cdlemefrs27.a . . . 4
42, 3atbase 32926 . . 3
5 cdleme29frs.o . . . 4
6 eqid 2471 . . . 4
75, 6cdleme31so 34017 . . 3
81, 4, 73syl 18 . 2
9 ssid 3437 . . . 4
109a1i 11 . . 3
11 simpll 768 . . . . . . . 8
12 simpr 468 . . . . . . . 8
1311, 12jca 541 . . . . . . 7
1413imim1i 59 . . . . . 6
1514ralimi 2796 . . . . 5
1615rgenw 2768 . . . 4
1716a1i 11 . . 3
18 cdlemefrs27.l . . . . 5
19 cdlemefrs27.j . . . . 5
20 cdlemefrs27.m . . . . 5
21 cdlemefrs27.h . . . . 5
22 cdlemefrs27.eq . . . . 5
23 cdlemefrs27.nb . . . . 5
24 cdlemefrs27.rnb . . . . 5
252, 18, 19, 20, 3, 21, 22, 23, 24cdlemefrs29bpre1 34035 . . . 4
26 simpl11 1105 . . . . . . . 8
27 simpl2r 1084 . . . . . . . 8
28 simpl3 1035 . . . . . . . 8
29 simpr 468 . . . . . . . 8
302, 18, 19, 20, 3, 21, 22cdlemefrs29pre00 34033 . . . . . . . 8
3126, 27, 28, 29, 30syl31anc 1295 . . . . . . 7
3231imbi1d 324 . . . . . 6
3332ralbidva 2828 . . . . 5
3433rexbidv 2892 . . . 4
3525, 34mpbid 215 . . 3
362, 18, 19, 20, 3, 21, 22, 23, 24cdlemefrs29cpre1 34036 . . 3
37 riotass2 6296 . . 3
3810, 17, 35, 36, 37syl22anc 1293 . 2
392, 18, 19, 20, 3, 21, 22, 23cdlemefrs29bpre0 34034 . . . 4