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 ) )

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 ) )

Step

Hyp

Ref

Expression

da.ps0

 |-  ( ps <-> ( ( c e. A /\ d e. A ) /\ -. c .<_ Y /\ ( d =/= c /\ -. d .<_ Y /\ C .<_ ( c .\/ d ) ) ) )

 |-  ( ( ( c e. A /\ d e. A ) /\ -. c .<_ Y /\ ( d =/= c /\ -. d .<_ Y /\ C .<_ ( c .\/ d ) ) ) -> C .<_ ( c .\/ d ) )

1 2

 |-  ( ps -> C .<_ ( c .\/ d ) )