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

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
StepHypRef Expression
1 con4.1 . 2 a = b
21ax-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
  Copyright terms: Public domain W3C validator