Theorem con34b 318

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 211	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))

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

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 209

This theorem is referenced by:  mtt  366  pm4.14  816  dfbi3  1060  ifpdfbi  1081  r19.23v  3188  raldifsni  4754  dff14a  7250  weniso  7334  dfom2  7844  dfsup2  9387  wemapsolem  9495  pwfseqlem3  10615  indstr  12914  rpnnen2lem12  16240  algcvgblem  16594  isirred2  20449  isdomn2OLD  20741  isdomn3  20744  ist0-3  23385  mdegleb  26104  dchrelbas4  27284  toslublem  33111  tosglblem  33113  bj-exexalal  37013  bj-alcomexcom  37117  poimirlem25  38108  poimirlem30  38113  tsbi3  38598  ntrneikb  44634  fulltermc  50096  aacllem  50386