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  3168  raldifsni  4771  dff14a  7263  weniso  7347  dfom2  7863  dfsup2  9456  wemapsolem  9564  pwfseqlem3  10674  indstr  12932  rpnnen2lem12  16243  algcvgblem  16596  isirred2  20381  isdomn2OLD  20672  isdomn3  20675  ist0-3  23283  mdegleb  26021  dchrelbas4  27206  toslublem  32952  tosglblem  32954  bj-alcomexcom  36698  poimirlem25  37669  poimirlem30  37674  tsbi3  38159  ntrneikb  44118  fulltermc  49396  aacllem  49665