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  829  nancom  1488  nic-ax  1677  nic-axALT  1678  alimex  1834  dfdif3  4045  ssconb  4068  disjsn  4644  oneqmini  6302  kmlem4  9840  isprm3  16316  bnj1171  32880  bnj1176  32885  bnj1204  32892  bnj1388  32913  bnj1523  32951  fvineqsneq  35510  dfxor5  41264  pm13.196a  41921