Theorem con34b 305

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 149	. 2 ⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))
2		con4 112	. 2 ⊢ ((¬ 𝜓 → ¬ 𝜑) → (𝜑 → 𝜓))
3	1, 2	impbii 199	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  mtt  353  pm4.14  601  dfbi3  1018  19.23t  2117  19.23tOLD  2254  r19.23v  3052  raldifsni  4357  dff14a  6567  weniso  6644  dfom2  7109  dfsup2  8391  wemapsolem  8496  pwfseqlem3  9520  indstr  11794  rpnnen2lem12  14998  algcvgblem  15337  isirred2  18747  isdomn2  19347  ist0-3  21197  mdegleb  23869  dchrelbas4  25013  toslublem  29795  tosglblem  29797  poimirlem25  33564  poimirlem30  33569  tsbi3  34072  isdomn3  38099  ntrneikb  38709  conss34OLD  38963  aacllem  42875