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  1496  nic-ax  1673  nic-axALT  1674  alimex  1831  dfdif3OLD  4071  ssconb  4095  disjsn  4665  oneqmini  6364  kmlem4  10067  isprm3  16612  ssdifidlprm  33405  bnj1171  34966  bnj1176  34971  bnj1204  34978  bnj1388  34999  bnj1523  35037  fvineqsneq  37385  dfxor5  43740  pm13.196a  44387  sswfaxreg  44961