Theorem con2b 361

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

Assertion

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

Proof of Theorem con2b

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

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

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 209

This theorem is referenced by:  mt2bi  365  pm4.15  843  nancom  1515  nic-ax  1692  nic-axALT  1693  alimex  1850  dfdif3OLD  4072  ssconb  4095  disjsn  4669  oneqmini  6395  kmlem4  10107  isprm3  16700  ssdifidlprm  33606  bnj1171  35259  bnj1176  35264  bnj1204  35271  bnj1388  35292  bnj1523  35330  regsfromsetind  36863  fvineqsneq  37870  dfxor5  44307  pm13.196a  44954  sswfaxreg  45527