Theorem con34b 319

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 156	. 2 ⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))
2		con4 113	. 2 ⊢ ((¬ 𝜓 → ¬ 𝜑) → (𝜑 → 𝜓))
3	1, 2	impbii 212	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))

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

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 210

This theorem is referenced by:  mtt  368  pm4.14  806  dfbi3  1045  ifpdfbi  1066  r19.23v  3238  raldifsni  4688  dff14a  7006  weniso  7086  dfom2  7562  dfsup2  8892  wemapsolem  8998  pwfseqlem3  10071  indstr  12304  rpnnen2lem12  15570  algcvgblem  15911  isirred2  19447  isdomn2  20065  ist0-3  21950  mdegleb  24665  dchrelbas4  25827  toslublem  30680  tosglblem  30682  poimirlem25  35082  poimirlem30  35087  tsbi3  35573  isdomn3  40148  ntrneikb  40797  aacllem  45329