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  803  dfbi3  1046  ifpdfbi  1067  r19.23v  3207  raldifsni  4725  dff14a  7124  weniso  7205  dfom2  7689  dfsup2  9133  wemapsolem  9239  pwfseqlem3  10347  indstr  12585  rpnnen2lem12  15862  algcvgblem  16210  isirred2  19858  isdomn2  20483  ist0-3  22404  mdegleb  25134  dchrelbas4  26296  toslublem  31152  tosglblem  31154  poimirlem25  35729  poimirlem30  35734  tsbi3  36220  isdomn3  40945  ntrneikb  41593  aacllem  46391