Theorem con1 66

Description: Contraposition inference. (Contributed by NM, 10-Aug-1997.)

Hypothesis

Ref	Expression
con1.1	a⊥ = b⊥

Assertion

Ref	Expression
con1	a = b

Proof of Theorem con1

Step	Hyp	Ref	Expression
1		con1.1	. . 3 a⊥ = b⊥
2	1	ax-r4 37	. 2 a⊥ ⊥ = b⊥ ⊥
3		ax-a1 30	. 2 a = a⊥ ⊥
4		ax-a1 30	. 2 b = b⊥ ⊥
5	2, 3, 4	3tr1 63	1 a = b

Syntax hints:   = wb 1  ^⊥ wn 4

This theorem was proved from axioms:  ax-a1 30  ax-r1 35  ax-r2 36  ax-r4 37

This theorem is referenced by:  wwcomd  214  k1-4  359  omla  447  fh3  471  fh4  472  u3lemnana  647  u5lemnana  649  u1lemnab  650  u2lemnab  651  u3lemnab  652  u4lemnab  653  u5lemnab  654  u1lemnanb  655  u2lemnanb  656  u3lemnanb  657  u4lemnanb  658  u5lemnanb  659  u1lemnoa  660  u2lemnoa  661  u3lemnoa  662  u4lemnoa  663  u5lemnoa  664  u1lemnona  665  u2lemnona  666  u3lemnona  667  u4lemnona  668  u5lemnona  669  u1lemnob  670  u2lemnob  671  u3lemnob  672  u4lemnob  673  u5lemnob  674  u1lemnonb  675  u3lemnonb  677  u4lemnonb  678  u5lemnonb  679  negantlem7  855  neg3antlem2  865  oa6to4  958  oa8to5  972  mldual  1124