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  806  dfbi3  1049  ifpdfbi  1070  r19.23v  3160  raldifsni  4746  dff14a  7210  weniso  7294  dfom2  7804  dfsup2  9335  wemapsolem  9443  pwfseqlem3  10558  indstr  12816  rpnnen2lem12  16136  algcvgblem  16490  isirred2  20341  isdomn2OLD  20629  isdomn3  20632  ist0-3  23261  mdegleb  25997  dchrelbas4  27182  toslublem  32960  tosglblem  32962  bj-alcomexcom  36745  poimirlem25  37705  poimirlem30  37710  tsbi3  38195  ntrneikb  44211  fulltermc  49636  aacllem  49926