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

Theorem 4atexlemk 30781
Description: Lemma for 4atexlem7 30809. (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 1652    e. wcel 1725    =/= wne 2598   class class class wbr 4204  (class class class)co 6073   HLchlt 30085
This theorem is referenced by:  4atexlemkl  30791  4atexlemkc  30792  4atexlempsb  30794  4atexlemqtb  30795  4atexlempns  30796  4atexlemu  30798  4atexlemv  30799  4atexlemunv  30800  4atexlemtlw  30801  4atexlemntlpq  30802  4atexlemc  30803  4atexlemnclw  30804  4atexlemex2  30805  4atexlemcnd  30806
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