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  1050  ifpdfbi  1071  r19.23v  3189  raldifsni  4820  dff14a  7307  weniso  7390  dfom2  7905  dfsup2  9513  wemapsolem  9619  pwfseqlem3  10729  indstr  12981  rpnnen2lem12  16273  algcvgblem  16624  isirred2  20447  isdomn2OLD  20734  isdomn3  20737  ist0-3  23374  mdegleb  26123  dchrelbas4  27305  toslublem  32945  tosglblem  32947  bj-alcomexcom  36646  poimirlem25  37605  poimirlem30  37610  tsbi3  38095  ntrneikb  44056  aacllem  48895