Theorem con2 67

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

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 37	. 2 a⊥ = b⊥ ⊥
3		ax-a1 30	. . 3 b = b⊥ ⊥
4	3	ax-r1 35	. 2 b⊥ ⊥ = b
5	2, 4	ax-r2 36	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:  anass  76  dfb  94  dfnb  95  an1  106  an0  108  anidm  111  anabs  121  mi  125  comm0  178  wwfh1  216  wwfh2  217  wwfh3  218  wwfh4  219  ka4lemo  228  ka4lem  229  ska10  238  lei3  246  ni31  250  0i1  273  ud1lem0c  277  ud2lem0c  278  ud4lem0c  280  ud5lem0c  281  wcom2an  428  omla  447  comcom  453  comd  456  comdr  466  com3i  467  df2c1  468  fh1  469  fh2  470  com2an  484  i3bi  496  ni32  502  lem4  511  i3th1  543  i3con  551  i3orlem5  556  ud1lem2  561  ud2lem2  564  ud4lem1a  577  ud4lem1c  579  ud4lem1  581  ud4lem2  582  ud5lem3c  593  u3lemob  632  u3lemonb  637  u5lemnaa  644  u1lemnab  650  u2lemnab  651  u3lemnab  652  u3lem1n  741  u5lem1n  743  u3lem3n  754  u4lem3n  755  u5lem3n  756  u4lem5n  766  u2lem7n  775  u3lem11a  787  gomaex3  924  lem3.3.4  1053