Metamath Proof Explorer


Theorem negcon2

Description: Negative contraposition law. (Contributed by NM, 14-Nov-2004)

Ref Expression
Assertion negcon2 A B A = B B = A

Proof

Step Hyp Ref Expression
1 negcon1 A B A = B B = A
2 eqcom A = B B = A
3 1 2 syl6rbbr A B A = B A = B
4 eqcom A = B B = A
5 3 4 syl6bb A B A = B B = A