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 154	. 2 ⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))
2		con4 114	. 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  367  pm4.14  818  dfbi3  1065  ifpdfbiOLD  1087  r19.23v  3192  raldifsni  4764  dff14a  7270  weniso  7354  dfom2  7865  dfsup2  9405  wemapsolem  9513  pwfseqlem3  10646  indstr  12941  rpnnen2lem12  16282  algcvgblem  16636  isirred2  20504  isdomn3  20800  ist0-3  23483  mdegleb  26202  dchrelbas4  27388  toslublem  33273  tosglblem  33275  bj-exexalal  37180  bj-alcomexcom  37284  poimirlem25  38277  poimirlem30  38282  tsbi3  38765  ntrneikb  44803  fulltermc  50272  aacllem  50584