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 39605
Description: Lemma for dath 39718. 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 1283 . 2 ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))) → 𝐾 ∈ HL)
31, 2sylbi 217 1 (𝜑𝐾 ∈ HL)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086  wcel 2105   class class class wbr 5147  cfv 6562  (class class class)co 7430  Basecbs 17244  HLchlt 39331
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 207  df-an 396  df-3an 1088
This theorem is referenced by:  dalemkelat  39606  dalemkeop  39607  dalempjqeb  39627  dalemsjteb  39628  dalemtjueb  39629  dalemqrprot  39630  dalempnes  39633  dalemqnet  39634  dalempjsen  39635  dalemply  39636  dalemsly  39637  dalemswapyz  39638  dalemrot  39639  dalemrotyz  39640  dalem1  39641  dalemcea  39642  dalem2  39643  dalemdea  39644  dalem3  39646  dalem4  39647  dalem5  39649  dalem-cly  39653  dalem9  39654  dalem11  39656  dalem12  39657  dalem13  39658  dalem15  39660  dalem16  39661  dalem17  39662  dalem18  39663  dalem19  39664  dalemswapyzps  39672  dalemcjden  39674  dalem21  39676  dalem22  39677  dalem23  39678  dalem24  39679  dalem25  39680  dalem27  39681  dalem28  39682  dalem38  39692  dalem39  39693  dalem41  39695  dalem42  39696  dalem43  39697  dalem44  39698  dalem45  39699  dalem51  39705  dalem52  39706  dalem54  39708  dalem55  39709  dalem56  39710  dalem57  39711  dalem58  39712  dalem59  39713  dalem60  39714
  Copyright terms: Public domain W3C validator