Theorem 4atexlemp 35336

Description: Lemma for 4atexlem7 35361. (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
4atexlemp	|- ( ph -> P e. A )

Proof of Theorem 4atexlemp

Step	Hyp	Ref	Expression
1		4thatlem.ph	. . 3 |- ( 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	1	4atexlempw 35335	. 2 |- ( ph -> ( P e. A /\ -. P .<_ W ) )
3	2	simpld 475	1 |- ( ph -> P e. A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   class class class wbr 4653  (class class class)co 6650   HLchlt 34637

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  4atexlempsb  35346  4atexlempns  35348  4atexlemswapqr  35349  4atexlemunv  35352  4atexlemtlw  35353  4atexlemc  35355  4atexlemex2  35357  4atexlemcnd  35358