Theorem con2b 360

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 208	1 ⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑))

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

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 206

This theorem is referenced by:  mt2bi  364  pm4.15  830  nancom  1491  nic-ax  1676  nic-axALT  1677  alimex  1833  dfdif3  4049  ssconb  4072  disjsn  4647  oneqmini  6317  kmlem4  9909  isprm3  16388  bnj1171  32980  bnj1176  32985  bnj1204  32992  bnj1388  33013  bnj1523  33051  fvineqsneq  35583  dfxor5  41375  pm13.196a  42032