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 ⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  mt2bi  366  pm4.15  846  nancom  1525  nic-ax  1705  nic-axALT  1706  alimex  1863  ssconb  4078  disjsn  4668  oneqmini  6416  kmlem4  10235  isprm3  16863  ssdifidlprm  21647  bnj1171  35676  bnj1176  35681  bnj1204  35688  bnj1388  35709  bnj1523  35747  regsfromsetind  37419  fvineqsneq  38428  dfxor5  44860  pm13.196a  45491  sswfaxreg  46070