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 eqcom A = B B = A
2 negcon1 A B A = B B = A
3 1 2 bitr4id A B A = B A = B
4 eqcom A = B B = A
5 3 4 bitrdi A B A = B B = A