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

Theorem cdlemesner 30718
 Description: Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012.)
Hypotheses
Ref Expression
cdlemesner.l
cdlemesner.j
cdlemesner.a
cdlemesner.h
Assertion
Ref Expression
cdlemesner

Proof of Theorem cdlemesner
StepHypRef Expression
1 nbrne2 4185 . . 3
213ad2ant3 980 . 2
32necomd 2647 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 359   w3a 936   wceq 1649   wcel 1721   wne 2564   class class class wbr 4167  cfv 5408  (class class class)co 6034  cple 13477  cjn 14342  catm 29686  chlt 29773  clh 30406 This theorem is referenced by:  cdlemeda  30720 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-rab 2672  df-v 2915  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-nul 3586  df-if 3697  df-sn 3777  df-pr 3778  df-op 3780  df-br 4168
 Copyright terms: Public domain W3C validator