Theorem con2b 360

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

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

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 208

This theorem is referenced by:  mt2bi  364  pm4.15  838  nancom  1503  nic-ax  1680  nic-axALT  1681  alimex  1838  dfdif3OLD  4056  ssconb  4079  disjsn  4650  oneqmini  6370  kmlem4  10074  isprm3  16650  ssdifidlprm  33548  bnj1171  35189  bnj1176  35194  bnj1204  35201  bnj1388  35222  bnj1523  35260  regsfromsetind  36774  fvineqsneq  37781  dfxor5  44218  pm13.196a  44865  sswfaxreg  45438