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  4799  dff14a  7269  weniso  7351  dfom2  7857  dfsup2  9439  wemapsolem  9545  pwfseqlem3  10655  indstr  12900  rpnnen2lem12  16168  algcvgblem  16514  isirred2  20235  isdomn2  20915  ist0-3  22849  mdegleb  25582  dchrelbas4  26746  toslublem  32142  tosglblem  32144  bj-alcomexcom  35558  poimirlem25  36513  poimirlem30  36518  tsbi3  37003  isdomn3  41946  ntrneikb  42845  aacllem  47848