Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  4atexlemk Unicode version

Theorem 4atexlemk 30163
Description: Lemma for 4atexlem7 30191. (Contributed by NM, 23-Nov-2012.)
Hypothesis
Ref Expression
4thatlem.ph  |-  ( ph  <->  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( S  e.  A  /\  ( R  e.  A  /\  -.  R  .<_  W  /\  ( P  .\/  R )  =  ( Q  .\/  R ) )  /\  ( T  e.  A  /\  ( U  .\/  T )  =  ( V  .\/  T ) ) )  /\  ( P  =/=  Q  /\  -.  S  .<_  ( P 
.\/  Q ) ) ) )
Assertion
Ref Expression
4atexlemk  |-  ( ph  ->  K  e.  HL )

Proof of Theorem 4atexlemk
StepHypRef Expression
1 4thatlem.ph . 2  |-  ( ph  <->  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( S  e.  A  /\  ( R  e.  A  /\  -.  R  .<_  W  /\  ( P  .\/  R )  =  ( Q  .\/  R ) )  /\  ( T  e.  A  /\  ( U  .\/  T )  =  ( V  .\/  T ) ) )  /\  ( P  =/=  Q  /\  -.  S  .<_  ( P 
.\/  Q ) ) ) )
2 simp11l 1068 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( S  e.  A  /\  ( R  e.  A  /\  -.  R  .<_  W  /\  ( P  .\/  R )  =  ( Q  .\/  R ) )  /\  ( T  e.  A  /\  ( U  .\/  T )  =  ( V  .\/  T ) ) )  /\  ( P  =/=  Q  /\  -.  S  .<_  ( P 
.\/  Q ) ) )  ->  K  e.  HL )
31, 2sylbi 188 1  |-  ( ph  ->  K  e.  HL )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1717    =/= wne 2552   class class class wbr 4155  (class class class)co 6022   HLchlt 29467
This theorem is referenced by:  4atexlemkl  30173  4atexlemkc  30174  4atexlempsb  30176  4atexlemqtb  30177  4atexlempns  30178  4atexlemu  30180  4atexlemv  30181  4atexlemunv  30182  4atexlemtlw  30183  4atexlemntlpq  30184  4atexlemc  30185  4atexlemnclw  30186  4atexlemex2  30187  4atexlemcnd  30188
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator