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  806  dfbi3  1049  ifpdfbi  1070  r19.23v  3183  raldifsni  4797  dff14a  7264  weniso  7346  dfom2  7852  dfsup2  9435  wemapsolem  9541  pwfseqlem3  10651  indstr  12896  rpnnen2lem12  16164  algcvgblem  16510  isirred2  20224  isdomn2  20902  ist0-3  22831  mdegleb  25564  dchrelbas4  26726  toslublem  32120  tosglblem  32122  bj-alcomexcom  35496  poimirlem25  36451  poimirlem30  36456  tsbi3  36941  isdomn3  41879  ntrneikb  42778  aacllem  47750