Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cdlemesner Structured version   Visualization version   GIF version

Theorem cdlemesner 36095
Description: Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012.)
Hypotheses
Ref Expression
cdlemesner.l = (le‘𝐾)
cdlemesner.j = (join‘𝐾)
cdlemesner.a 𝐴 = (Atoms‘𝐾)
cdlemesner.h 𝐻 = (LHyp‘𝐾)
Assertion
Ref Expression
cdlemesner ((𝐾 ∈ HL ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑆𝑅)

Proof of Theorem cdlemesner
StepHypRef Expression
1 nbrne2 4875 . . 3 ((𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄)) → 𝑅𝑆)
213ad2ant3 1158 . 2 ((𝐾 ∈ HL ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑅𝑆)
32necomd 3044 1 ((𝐾 ∈ HL ∧ (𝑅𝐴𝑆𝐴) ∧ (𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑆𝑅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  w3a 1100   = wceq 1637  wcel 2157  wne 2989   class class class wbr 4855  cfv 6111  (class class class)co 6884  lecple 16180  joincjn 17169  Atomscatm 35062  HLchlt 35149  LHypclh 35783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-br 4856
This theorem is referenced by:  cdlemeda  36097
  Copyright terms: Public domain W3C validator