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 40430
Description: Lemma for dath 40543. 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 1303 . 2 ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))) → 𝐾 ∈ HL)
31, 2sylbi 220 1 (𝜑𝐾 ∈ HL)
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  ¬ wn 3  wi 4  wb 209  wa 401  w3a 1103  wcel 2146   class class class wbr 5114  cfv 6543  (class class class)co 7423  Basecbs 17294  HLchlt 40157
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105
This theorem is used by:  dalemkelat  40431  dalemkeop  40432  dalempjqeb  40452  dalemsjteb  40453  dalemtjueb  40454  dalemqrprot  40455  dalempnes  40458  dalemqnet  40459  dalempjsen  40460  dalemply  40461  dalemsly  40462  dalemswapyz  40463  dalemrot  40464  dalemrotyz  40465  dalem1  40466  dalemcea  40467  dalem2  40468  dalemdea  40469  dalem3  40471  dalem4  40472  dalem5  40474  dalem-cly  40478  dalem9  40479  dalem11  40481  dalem12  40482  dalem13  40483  dalem15  40485  dalem16  40486  dalem17  40487  dalem18  40488  dalem19  40489  dalemswapyzps  40497  dalemcjden  40499  dalem21  40501  dalem22  40502  dalem23  40503  dalem24  40504  dalem25  40505  dalem27  40506  dalem28  40507  dalem38  40517  dalem39  40518  dalem41  40520  dalem42  40521  dalem43  40522  dalem44  40523  dalem45  40524  dalem51  40530  dalem52  40531  dalem54  40533  dalem55  40534  dalem56  40535  dalem57  40536  dalem58  40537  dalem59  40538  dalem60  40539
  Copyright terms: Public domain W3C validator