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  833  nancom  1498  nic-ax  1675  nic-axALT  1676  alimex  1833  dfdif3OLD  4058  ssconb  4082  disjsn  4655  oneqmini  6376  kmlem4  10076  isprm3  16652  ssdifidlprm  33518  bnj1171  35142  bnj1176  35147  bnj1204  35154  bnj1388  35175  bnj1523  35213  regsfromsetind  36721  fvineqsneq  37728  dfxor5  44194  pm13.196a  44841  sswfaxreg  45414