Theorem con2b 362

Description: Contraposition. Bidirectional version of con2 136. (Contributed by NM, 12-Mar-1993.)

Assertion

Ref	Expression
con2b	⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑))

Proof of Theorem con2b

Step	Hyp	Ref	Expression
1		con2 136	. 2 ⊢ ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑))
2		con2 136	. 2 ⊢ ((𝜓 → ¬ 𝜑) → (𝜑 → ¬ 𝜓))
3	1, 2	impbii 212	1 ⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑))

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

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 210

This theorem is referenced by:  mt2bi  366  pm4.15  845  nancom  1519  nic-ax  1696  nic-axALT  1697  alimex  1854  dfdif3OLD  4075  ssconb  4098  disjsn  4673  oneqmini  6403  kmlem4  10125  isprm3  16731  ssdifidlprm  21446  bnj1171  35305  bnj1176  35310  bnj1204  35317  bnj1388  35338  bnj1523  35376  regsfromsetind  36912  fvineqsneq  37918  dfxor5  44355  pm13.196a  44988  sswfaxreg  45561