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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  mt2bi  366  pm4.15  846  nancom  1526  nic-ax  1706  nic-axALT  1707  alimex  1864  ssconb  4081  disjsn  4672  oneqmini  6434  kmlem4  10259  isprm3  16887  ssdifidlprm  21672  bnj1171  35700  bnj1176  35705  bnj1204  35712  bnj1388  35733  bnj1523  35771  regsfromsetind  37505  fvineqsneq  38527  dfxor5  44959  pm13.196a  45590  sswfaxreg  46172