Theorem con34b 315

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  364  pm4.14  804  dfbi3  1047  ifpdfbi  1068  r19.23v  3175  raldifsni  4741  dff14a  7193  weniso  7275  dfom2  7774  dfsup2  9293  wemapsolem  9399  pwfseqlem3  10509  indstr  12749  rpnnen2lem12  16025  algcvgblem  16371  isirred2  20030  isdomn2  20668  ist0-3  22594  mdegleb  25327  dchrelbas4  26489  toslublem  31450  tosglblem  31452  bj-alcomexcom  34953  poimirlem25  35900  poimirlem30  35905  tsbi3  36391  isdomn3  41280  ntrneikb  42014  aacllem  46845