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  3156  raldifsni  4749  dff14a  7211  weniso  7295  dfom2  7808  dfsup2  9353  wemapsolem  9461  pwfseqlem3  10573  indstr  12835  rpnnen2lem12  16152  algcvgblem  16506  isirred2  20324  isdomn2OLD  20615  isdomn3  20618  ist0-3  23248  mdegleb  25985  dchrelbas4  27170  toslublem  32927  tosglblem  32929  bj-alcomexcom  36653  poimirlem25  37624  poimirlem30  37629  tsbi3  38114  ntrneikb  44067  fulltermc  49497  aacllem  49787