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

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

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 207

This theorem is referenced by:  mt2bi  363  pm4.15  832  nancom  1497  nic-ax  1674  nic-axALT  1675  alimex  1832  dfdif3OLD  4070  ssconb  4094  disjsn  4668  oneqmini  6370  kmlem4  10064  isprm3  16610  ssdifidlprm  33539  bnj1171  35156  bnj1176  35161  bnj1204  35168  bnj1388  35189  bnj1523  35227  regsfromsetind  36669  fvineqsneq  37613  dfxor5  44004  pm13.196a  44651  sswfaxreg  45224