Theorem con1 66

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

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

Copyright terms: Public domain