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  831  nancom  1494  nic-ax  1675  nic-axALT  1676  alimex  1833  dfdif3  4114  ssconb  4137  disjsn  4715  oneqmini  6416  kmlem4  10147  isprm3  16619  bnj1171  34006  bnj1176  34011  bnj1204  34018  bnj1388  34039  bnj1523  34077  fvineqsneq  36288  dfxor5  42508  pm13.196a  43163