Theorem con1 63

Description: Contraposition inference.

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 36	. 2 a⊥ ⊥ = b⊥ ⊥
3		ax-a1 29	. 2 a = a⊥ ⊥
4		ax-a1 29	. 2 b = b⊥ ⊥
5	2, 3, 4	3tr1 60	1 a = b

Syntax hints:   = wb 1  ^⊥ wn 4

This theorem is referenced by:  wwcomd 206  omla 429  fh3 453  fh4 454  u3lemnana 629  u5lemnana 631  u1lemnab 632  u2lemnab 633  u3lemnab 634  u4lemnab 635  u5lemnab 636  u1lemnanb 637  u2lemnanb 638  u3lemnanb 639  u4lemnanb 640  u5lemnanb 641  u1lemnoa 642  u2lemnoa 643  u3lemnoa 644  u4lemnoa 645  u5lemnoa 646  u1lemnona 647  u2lemnona 648  u3lemnona 649  u4lemnona 650  u5lemnona 651  u1lemnob 652  u2lemnob 653  u3lemnob 654  u4lemnob 655  u5lemnob 656  u1lemnonb 657  u3lemnonb 659  u4lemnonb 660  u5lemnonb 661  negantlem7 837  neg3antlem2 847  oa6to4 938  oa8to5 952

This theorem was proved from axioms:  ax-a1 29  ax-r1 34  ax-r2 35  ax-r4 36

metamath.org