Theorem con2b 362

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

Assertion

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

Proof of Theorem con2b

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

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

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 209

This theorem is referenced by:  mt2bi  366  pm4.15  830  nancom  1486  nic-ax  1674  nic-axALT  1675  alimex  1831  dfdif3  4093  ssconb  4116  disjsn  4649  oneqmini  6244  kmlem4  9581  isprm3  16029  bnj1171  32274  bnj1176  32279  bnj1204  32286  bnj1388  32307  bnj1523  32345  fvineqsneq  34695  dfxor5  40119  pm13.196a  40753