Theorem con34b 316

Description: A biconditional form of contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116. (Contributed by NM, 11-May-1993.)

Assertion

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

Proof of Theorem con34b

Step	Hyp	Ref	Expression
1		con3 153	. 2 ⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))
2		con4 113	. 2 ⊢ ((¬ 𝜓 → ¬ 𝜑) → (𝜑 → 𝜓))
3	1, 2	impbii 209	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))

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

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 207

This theorem is referenced by:  mtt  364  pm4.14  807  dfbi3  1050  ifpdfbi  1071  r19.23v  3164  raldifsni  4740  dff14a  7225  weniso  7309  dfom2  7819  dfsup2  9357  wemapsolem  9465  pwfseqlem3  10583  indstr  12866  rpnnen2lem12  16192  algcvgblem  16546  isirred2  20401  isdomn2OLD  20689  isdomn3  20692  ist0-3  23310  mdegleb  26029  dchrelbas4  27206  toslublem  33032  tosglblem  33034  bj-exexalal  36871  bj-alcomexcom  36975  poimirlem25  37966  poimirlem30  37971  tsbi3  38456  ntrneikb  44521  fulltermc  49986  aacllem  50276