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

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

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 206

This theorem is referenced by:  mt2bi  364  pm4.15  832  nancom  1495  nic-ax  1676  nic-axALT  1677  alimex  1834  dfdif3  4115  ssconb  4138  disjsn  4716  oneqmini  6417  kmlem4  10148  isprm3  16620  bnj1171  34011  bnj1176  34016  bnj1204  34023  bnj1388  34044  bnj1523  34082  fvineqsneq  36293  dfxor5  42518  pm13.196a  43173