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  1526  nic-ax  1706  nic-axALT  1707  alimex  1864  ssconb  4092  disjsn  4675  oneqmini  6415  kmlem4  10160  isprm3  16779  ssdifidlprm  21555  bnj1171  35517  bnj1176  35522  bnj1204  35529  bnj1388  35550  bnj1523  35588  regsfromsetind  37166  fvineqsneq  38174  dfxor5  44615  pm13.196a  45246  sswfaxreg  45818