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  807  dfbi3  1050  ifpdfbi  1071  r19.23v  3165  raldifsni  4753  dff14a  7226  weniso  7310  dfom2  7820  dfsup2  9359  wemapsolem  9467  pwfseqlem3  10583  indstr  12841  rpnnen2lem12  16162  algcvgblem  16516  isirred2  20369  isdomn2OLD  20657  isdomn3  20660  ist0-3  23301  mdegleb  26037  dchrelbas4  27222  toslublem  33064  tosglblem  33066  bj-exexalal  36827  bj-alcomexcom  36919  poimirlem25  37890  poimirlem30  37895  tsbi3  38380  ntrneikb  44444  fulltermc  49864  aacllem  50154