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 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:  mtt  365  pm4.14  804  dfbi3  1047  ifpdfbi  1068  r19.23v  3208  raldifsni  4728  dff14a  7143  weniso  7225  dfom2  7714  dfsup2  9203  wemapsolem  9309  pwfseqlem3  10416  indstr  12656  rpnnen2lem12  15934  algcvgblem  16282  isirred2  19943  isdomn2  20570  ist0-3  22496  mdegleb  25229  dchrelbas4  26391  toslublem  31250  tosglblem  31252  poimirlem25  35802  poimirlem30  35807  tsbi3  36293  isdomn3  41029  ntrneikb  41704  aacllem  46505