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  dfdif3OLD  4076  ssconb  4099  disjsn  4682  oneqmini  6421  kmlem4  10156  isprm3  16766  ssdifidlprm  21523  bnj1171  35420  bnj1176  35425  bnj1204  35432  bnj1388  35453  bnj1523  35491  regsfromsetind  37091  fvineqsneq  38099  dfxor5  44534  pm13.196a  45165  sswfaxreg  45737