Metamath Proof Explorer


Theorem dalemclccjdd

Description: Lemma for dath . Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012)

Ref Expression
Hypothesis da.ps0
|- ( ps <-> ( ( c e. A /\ d e. A ) /\ -. c .<_ Y /\ ( d =/= c /\ -. d .<_ Y /\ C .<_ ( c .\/ d ) ) ) )
Assertion dalemclccjdd
|- ( ps -> C .<_ ( c .\/ d ) )

Proof

Step Hyp Ref Expression
1 da.ps0
 |-  ( ps <-> ( ( c e. A /\ d e. A ) /\ -. c .<_ Y /\ ( d =/= c /\ -. d .<_ Y /\ C .<_ ( c .\/ d ) ) ) )
2 simp33
 |-  ( ( ( c e. A /\ d e. A ) /\ -. c .<_ Y /\ ( d =/= c /\ -. d .<_ Y /\ C .<_ ( c .\/ d ) ) ) -> C .<_ ( c .\/ d ) )
3 1 2 sylbi
 |-  ( ps -> C .<_ ( c .\/ d ) )