Theorem con2b 363

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

Assertion

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

Proof of Theorem con2b

Step	Hyp	Ref	Expression
1		con2 137	. 2 ⊢ ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑))
2		con2 137	. 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  367  pm4.15  831  nancom  1487  nic-ax  1675  nic-axALT  1676  alimex  1832  dfdif3  4042  ssconb  4065  disjsn  4607  oneqmini  6210  kmlem4  9564  isprm3  16017  bnj1171  32382  bnj1176  32387  bnj1204  32394  bnj1388  32415  bnj1523  32453  fvineqsneq  34829  dfxor5  40468  pm13.196a  41118