Theorem lecon2 156

Description: Contrapositive for l.e. (Contributed by NM, 19-Dec-1998.)

Hypothesis

Ref	Expression
lecon2.1	a⊥ ≤ b

Assertion

Ref	Expression
lecon2	b⊥ ≤ a

Proof of Theorem lecon2

Step	Hyp	Ref	Expression
1		lecon2.1	. . 3 a⊥ ≤ b
2		ax-a1 30	. . 3 b = b⊥ ⊥
3	1, 2	lbtr 139	. 2 a⊥ ≤ b⊥ ⊥
4	3	lecon1 155	1 b⊥ ≤ a

This proof depends on syntax axioms:   ≤ wle 2  ^⊥ wn 4

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This proof depends on definitions:  df-a 40  df-le1 130  df-le2 131

This theorem is used by:  lecon3  157  cancellem  891  kb10iii  893