Theorem lecon 146

Description: Contrapositive for l.e.

Hypothesis

Ref	Expression
le.1	a =< b

Assertion

Ref	Expression
lecon	b_|_ =< a_|_

Proof of Theorem lecon

Step	Hyp	Ref	Expression
1		ax-a2 30	. . . 4 (b v a) = (a v b)
2		oran 79	. . . 4 (b v a) = (b_|_ ^ a_|_)_|_
3		le.1	. . . . 5 a =< b
4	3	df-le2 123	. . . 4 (a v b) = b
5	1, 2, 4	3tr2 61	. . 3 (b_|_ ^ a_|_)_|_ = b
6	5	con3 65	. 2 (b_|_ ^ a_|_) = b_|_
7	6	df2le1 127	1 b_|_ =< a_|_

Syntax hints:   =< wle 2  _|_wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  lecon1 147  lecon3 149  lei3 238  nom14 303  i2or 336  ska4 415  binr1 499  ud4lem1a 559  biao 781  3vded12 797  3vded22 800  3vroa 813  sa5 818  elimconslem 849  comanb 854  marsdenlem3 864  gomaex3h4 885  gomaex3h7 888  gomaex3h11 892  oa3to4lem6 930  oa6todual 932  oa6fromdual 933  oa4to6 945  oa8todual 951

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-a 39  df-le1 122  df-le2 123

metamath.org