con4 - Quantum Logic Explorer

	Quantum Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > QLE Home > Th. List > con4		GIF version

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^⊥

Colors of variables: term

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