Theorem con3 68

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

Hypothesis

Ref	Expression
con3.1	a⊥ = b

Assertion

Ref	Expression
con3	a = b⊥

Proof of Theorem con3

Step	Hyp	Ref	Expression
1		ax-a1 30	. 2 a = a⊥ ⊥
2		con3.1	. . 3 a⊥ = b
3	2	ax-r4 37	. 2 a⊥ ⊥ = b⊥
4	1, 3	ax-r2 36	1 a = b⊥

Syntax hints:   = wb 1  ^⊥ wn 4

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

This theorem is referenced by:  anor3  90  oran1  91  oran2  92  oran3  93  lecon  154  wlem3.1  210  wwcomd  214  wwfh1  216  ud1lem0c  277  nom12  309  nom13  310  comd  456  fh1  469  i3bi  496  ud1lem3  562  ud2lem2  564  ud3lem1a  566  ud3lem2  571  ud4lem1a  577  ud4lem2  582  ud5lem1b  587  ud5lem1  589  ud5lem3  594  u4lemona  628  u2lemnonb  676  oa6to4h1  955  oa6to4h2  956  oa6to4h3  957  lem3.3.4  1053