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 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  363  pm4.15  832  nancom  1490  nic-ax  1668  nic-axALT  1669  alimex  1826  dfdif3  4110  ssconb  4133  disjsn  4711  oneqmini  6415  kmlem4  10162  isprm3  16639  bnj1171  34554  bnj1176  34559  bnj1204  34566  bnj1388  34587  bnj1523  34625  fvineqsneq  36814  dfxor5  43110  pm13.196a  43764