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 36819
Description: Lemma for dath 36932. 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 1281 . 2 ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))) → 𝐾 ∈ HL)
31, 2sylbi 220 1 (𝜑𝐾 ∈ HL)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084  wcel 2115   class class class wbr 5047  cfv 6336  (class class class)co 7138  Basecbs 16472  HLchlt 36546
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  dalemkelat  36820  dalemkeop  36821  dalempjqeb  36841  dalemsjteb  36842  dalemtjueb  36843  dalemqrprot  36844  dalempnes  36847  dalemqnet  36848  dalempjsen  36849  dalemply  36850  dalemsly  36851  dalemswapyz  36852  dalemrot  36853  dalemrotyz  36854  dalem1  36855  dalemcea  36856  dalem2  36857  dalemdea  36858  dalem3  36860  dalem4  36861  dalem5  36863  dalem-cly  36867  dalem9  36868  dalem11  36870  dalem12  36871  dalem13  36872  dalem15  36874  dalem16  36875  dalem17  36876  dalem18  36877  dalem19  36878  dalemswapyzps  36886  dalemcjden  36888  dalem21  36890  dalem22  36891  dalem23  36892  dalem24  36893  dalem25  36894  dalem27  36895  dalem28  36896  dalem38  36906  dalem39  36907  dalem41  36909  dalem42  36910  dalem43  36911  dalem44  36912  dalem45  36913  dalem51  36919  dalem52  36920  dalem54  36922  dalem55  36923  dalem56  36924  dalem57  36925  dalem58  36926  dalem59  36927  dalem60  36928
  Copyright terms: Public domain W3C validator