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  4089  disjsn  4672  oneqmini  6409  kmlem4  10213  isprm3  16838  ssdifidlprm  21622  bnj1171  35613  bnj1176  35618  bnj1204  35625  bnj1388  35646  bnj1523  35684  regsfromsetind  37297  fvineqsneq  38303  dfxor5  44726  pm13.196a  45357  sswfaxreg  45929