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  3162  raldifsni  4762  dff14a  7248  weniso  7332  dfom2  7847  dfsup2  9402  wemapsolem  9510  pwfseqlem3  10620  indstr  12882  rpnnen2lem12  16200  algcvgblem  16554  isirred2  20337  isdomn2OLD  20628  isdomn3  20631  ist0-3  23239  mdegleb  25976  dchrelbas4  27161  toslublem  32905  tosglblem  32907  bj-alcomexcom  36675  poimirlem25  37646  poimirlem30  37651  tsbi3  38136  ntrneikb  44090  fulltermc  49504  aacllem  49794