Theorem con4 69

Description: Contraposition inference. (Contributed by NM, 26-May-2008.) (Revised by NM, 31-Mar-2011.)

Hypothesis

Ref	Expression
con4.1	a = b

Assertion

Ref	Expression
con4	a⊥ = b⊥

Proof of Theorem con4

Step	Hyp	Ref	Expression
1		con4.1	. 2 a = b
2	1	ax-r4 37	1 a⊥ = b⊥

Syntax hints:   = wb 1  ^⊥ wn 4

This theorem was proved from axioms:  ax-r4 37

This theorem is referenced by:  k1-6  353  k1-7  354