Theorem con4 69

Description: Contraposition inference.

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 is referenced by:  k1-6 353  k1-7 354

This theorem was proved from axioms:  ax-r4 37

Copyright terms: Public domain