Theorem con2 64

Description: Contraposition inference.

Hypothesis

Ref	Expression
con2.1	a = b⊥

Assertion

Ref	Expression
con2	a⊥ = b

Proof of Theorem con2

Step	Hyp	Ref	Expression
1		con2.1	. . 3 a = b⊥
2	1	ax-r4 36	. 2 a⊥ = b⊥ ⊥
3		ax-a1 29	. . 3 b = b⊥ ⊥
4	3	ax-r1 34	. 2 b⊥ ⊥ = b
5	2, 4	ax-r2 35	1 a⊥ = b

Syntax hints:   = wb 1  ^⊥ wn 4

This theorem is referenced by:  anass 69  dfb 86  dfnb 87  an1 98  an0 100  anidm 103  a5c 113  mi 117  comm0 170  wwfh1 208  wwfh2 209  wwfh3 210  wwfh4 211  ka4lemo 220  ka4lem 221  ska10 230  lei3 238  ni31 242  0i1 265  ud1lem0c 269  ud2lem0c 270  ud4lem0c 272  ud5lem0c 273  wcom2an 410  omla 429  comcom 435  comd 438  comdr 448  com3i 449  df2c1 450  fh1 451  fh2 452  com2an 466  i3bi 478  ni32 484  lem4 493  i3th1 525  i3con 533  i3orlem5 538  ud1lem2 543  ud2lem2 546  ud4lem1a 559  ud4lem1c 561  ud4lem1 563  ud4lem2 564  ud5lem3c 575  u3lemob 614  u3lemonb 619  u5lemnaa 626  u1lemnab 632  u2lemnab 633  u3lemnab 634  u3lem1n 723  u5lem1n 725  u3lem3n 736  u4lem3n 737  u5lem3n 738  u4lem5n 748  u2lem7n 757  u3lem11a 769  gomaex3 904

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

metamath.org