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 35648
Description: Lemma for dath 35761. 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 1384 . 2 ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (𝑌𝑂𝑍𝑂) ∧ ((¬ 𝐶 (𝑃 𝑄) ∧ ¬ 𝐶 (𝑄 𝑅) ∧ ¬ 𝐶 (𝑅 𝑃)) ∧ (¬ 𝐶 (𝑆 𝑇) ∧ ¬ 𝐶 (𝑇 𝑈) ∧ ¬ 𝐶 (𝑈 𝑆)) ∧ (𝐶 (𝑃 𝑆) ∧ 𝐶 (𝑄 𝑇) ∧ 𝐶 (𝑅 𝑈)))) → 𝐾 ∈ HL)
31, 2sylbi 209 1 (𝜑𝐾 ∈ HL)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 385  w3a 1108  wcel 2157   class class class wbr 4847  cfv 6105  (class class class)co 6882  Basecbs 16188  HLchlt 35375
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 199  df-an 386  df-3an 1110
This theorem is referenced by:  dalemkelat  35649  dalemkeop  35650  dalempjqeb  35670  dalemsjteb  35671  dalemtjueb  35672  dalemqrprot  35673  dalempnes  35676  dalemqnet  35677  dalempjsen  35678  dalemply  35679  dalemsly  35680  dalemswapyz  35681  dalemrot  35682  dalemrotyz  35683  dalem1  35684  dalemcea  35685  dalem2  35686  dalemdea  35687  dalem3  35689  dalem4  35690  dalem5  35692  dalem-cly  35696  dalem9  35697  dalem11  35699  dalem12  35700  dalem13  35701  dalem15  35703  dalem16  35704  dalem17  35705  dalem18  35706  dalem19  35707  dalemswapyzps  35715  dalemcjden  35717  dalem21  35719  dalem22  35720  dalem23  35721  dalem24  35722  dalem25  35723  dalem27  35724  dalem28  35725  dalem38  35735  dalem39  35736  dalem41  35738  dalem42  35739  dalem43  35740  dalem44  35741  dalem45  35742  dalem51  35748  dalem52  35749  dalem54  35751  dalem55  35752  dalem56  35753  dalem57  35754  dalem58  35755  dalem59  35756  dalem60  35757
  Copyright terms: Public domain W3C validator