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

Theorem dalemkehl 38494
Description: Lemma for dath 38607. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.)
Hypothesis
Ref Expression
dalema.ph (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))))
Assertion
Ref Expression
dalemkehl (𝜑𝐾 ∈ HL)

Proof of Theorem dalemkehl
StepHypRef Expression
1 dalema.ph . 2 (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))))
2 simp11l 1285 . 2 ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))) → 𝐾 ∈ HL)
31, 2sylbi 216 1 (𝜑𝐾 ∈ HL)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  w3a 1088  wcel 2107   class class class wbr 5149  cfv 6544  (class class class)co 7409  Basecbs 17144  HLchlt 38220
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090
This theorem is referenced by:  dalemkelat  38495  dalemkeop  38496  dalempjqeb  38516  dalemsjteb  38517  dalemtjueb  38518  dalemqrprot  38519  dalempnes  38522  dalemqnet  38523  dalempjsen  38524  dalemply  38525  dalemsly  38526  dalemswapyz  38527  dalemrot  38528  dalemrotyz  38529  dalem1  38530  dalemcea  38531  dalem2  38532  dalemdea  38533  dalem3  38535  dalem4  38536  dalem5  38538  dalem-cly  38542  dalem9  38543  dalem11  38545  dalem12  38546  dalem13  38547  dalem15  38549  dalem16  38550  dalem17  38551  dalem18  38552  dalem19  38553  dalemswapyzps  38561  dalemcjden  38563  dalem21  38565  dalem22  38566  dalem23  38567  dalem24  38568  dalem25  38569  dalem27  38570  dalem28  38571  dalem38  38581  dalem39  38582  dalem41  38584  dalem42  38585  dalem43  38586  dalem44  38587  dalem45  38588  dalem51  38594  dalem52  38595  dalem54  38597  dalem55  38598  dalem56  38599  dalem57  38600  dalem58  38601  dalem59  38602  dalem60  38603
  Copyright terms: Public domain W3C validator