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

Theorem dalemccea 30417
Description: Lemma for dath 30470. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.)
Hypothesis
Ref Expression
da.ps0  |-  ( ps  <->  ( ( c  e.  A  /\  d  e.  A
)  /\  -.  c  .<_  Y  /\  ( d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
) ) ) )
Assertion
Ref Expression
dalemccea  |-  ( ps 
->  c  e.  A
)

Proof of Theorem dalemccea
StepHypRef Expression
1 da.ps0 . 2  |-  ( ps  <->  ( ( c  e.  A  /\  d  e.  A
)  /\  -.  c  .<_  Y  /\  ( d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
) ) ) )
2 simp1l 981 . 2  |-  ( ( ( c  e.  A  /\  d  e.  A
)  /\  -.  c  .<_  Y  /\  ( d  =/=  c  /\  -.  d  .<_  Y  /\  C  .<_  ( c  .\/  d
) ) )  -> 
c  e.  A )
31, 2sylbi 188 1  |-  ( ps 
->  c  e.  A
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936    e. wcel 1725    =/= wne 2598   class class class wbr 4204  (class class class)co 6073
This theorem is referenced by:  dalemcceb  30423  dalemswapyzps  30424  dalemrotps  30425  dalemcjden  30426  dalem23  30430  dalem24  30431  dalem25  30432  dalem27  30433  dalem28  30434  dalem38  30444  dalem39  30445  dalem44  30450  dalem51  30457  dalem56  30462
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