Theorem con2b 359

Description: Contraposition. Bidirectional version of con2 135. (Contributed by NM, 12-Mar-1993.)

Assertion

Ref	Expression
con2b	⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑))

Proof of Theorem con2b

Step	Hyp	Ref	Expression
1		con2 135	. 2 ⊢ ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑))
2		con2 135	. 2 ⊢ ((𝜓 → ¬ 𝜑) → (𝜑 → ¬ 𝜓))
3	1, 2	impbii 209	1 ⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  mt2bi  363  pm4.15  833  nancom  1492  nic-ax  1669  nic-axALT  1670  alimex  1827  dfdif3OLD  4127  ssconb  4151  disjsn  4715  oneqmini  6437  kmlem4  10191  isprm3  16716  ssdifidlprm  33465  bnj1171  34992  bnj1176  34997  bnj1204  35004  bnj1388  35025  bnj1523  35063  fvineqsneq  37394  dfxor5  43756  pm13.196a  44409