Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cdlemd9 Unicode version

Theorem cdlemd9 34131
Description: Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Jun-2012.)
Hypotheses
Ref Expression
cdlemd4.l
cdlemd4.j
cdlemd4.a
cdlemd4.h
cdlemd4.t
Assertion
Ref Expression
cdlemd9

Proof of Theorem cdlemd9
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpl1 991 . . 3
2 simpl2 992 . . 3
3 simpl3 993 . . 3
4 simpr 461 . . 3
5 cdlemd4.l . . . 4
6 cdlemd4.j . . . 4
7 cdlemd4.a . . . 4
8 cdlemd4.h . . . 4
9 cdlemd4.t . . . 4
105, 6, 7, 8, 9cdlemd8 34130 . . 3
111, 2, 3, 4, 10syl112anc 1223 . 2
12 simpl11 1063 . . . 4
13 simpl2 992 . . . 4
14 simp12l 1101 . . . . . 6
1514adantr 465 . . . . 5
165, 7, 8, 9ltrnel 34064 . . . . 5
1712, 15, 13, 16syl3anc 1219 . . . 4
18 simpr 461 . . . . 5
1918necomd 2716 . . . 4
205, 6, 7, 8cdlemb2 33966 . . . 4
2112, 13, 17, 19, 20syl121anc 1224 . . 3
22 simp1l1 1081 . . . . 5
23 simp1l2 1082 . . . . 5
24 simp2 989 . . . . . 6
25 simp3l 1016 . . . . . 6
2624, 25jca 532 . . . . 5
27 simp1l3 1083 . . . . 5
28 simp3r 1017 . . . . 5
295, 6, 7, 8, 9cdlemd7 34129 . . . . 5
3022, 23, 26, 27, 28, 29syl122anc 1228 . . . 4
3130rexlimdv3a 2923 . . 3
3221, 31mpd 15 . 2
3311, 32pm2.61dane 2763 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  /\wa 369  /\w3a 965  =wceq 1370  e.wcel 1757  =/=wne 2641  E.wrex 2793   class class class wbr 4374  `cfv 5500  (class class class)co 6174   cple 14331   cjn 15200   catm 33189   chlt 33276   clh 33909   cltrn 34026
This theorem is referenced by:  cdlemd  34132
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-rep 4485  ax-sep 4495  ax-nul 4503  ax-pow 4552  ax-pr 4613  ax-un 6456
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-reu 2799  df-rab 2801  df-v 3054  df-sbc 3269  df-csb 3371  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-nul 3720  df-if 3874  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4174  df-iun 4255  df-iin 4256  df-br 4375  df-opab 4433  df-mpt 4434  df-id 4718  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-rn 4933  df-res 4934  df-ima 4935  df-iota 5463  df-fun 5502  df-fn 5503  df-f 5504  df-f1 5505  df-fo 5506  df-f1o 5507  df-fv 5508  df-riota 6135  df-ov 6177  df-oprab 6178  df-mpt2 6179  df-1st 6661  df-2nd 6662  df-map 7300  df-poset 15202  df-plt 15214  df-lub 15230  df-glb 15231  df-join 15232  df-meet 15233  df-p0 15295  df-p1 15296  df-lat 15302  df-clat 15364  df-oposet 33102  df-ol 33104  df-oml 33105  df-covers 33192  df-ats 33193  df-atl 33224  df-cvlat 33248  df-hlat 33277  df-llines 33423  df-psubsp 33428  df-pmap 33429  df-padd 33721  df-lhyp 33913  df-laut 33914  df-ldil 34029  df-ltrn 34030  df-trl 34084
  Copyright terms: Public domain W3C validator