Theorem con2b 362

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

Assertion

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

Proof of Theorem con2b

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

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

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 210

This theorem is referenced by:  mt2bi  366  pm4.15  845  nancom  1526  nic-ax  1703  nic-axALT  1704  alimex  1861  dfdif3OLD  4074  ssconb  4097  disjsn  4678  oneqmini  6416  kmlem4  10138  isprm3  16742  ssdifidlprm  21467  bnj1171  35366  bnj1176  35371  bnj1204  35378  bnj1388  35399  bnj1523  35437  regsfromsetind  37028  fvineqsneq  38036  dfxor5  44473  pm13.196a  45104  sswfaxreg  45676