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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  mtt  367  pm4.14  819  dfbi3  1065  ifpdfbiOLD  1087  r19.23v  3190  raldifsni  4758  dff14a  7266  weniso  7356  dfom2  7868  dfsup2  9420  wemapsolem  9528  pwfseqlem3  10726  indstr  13024  rpnnen2lem12  16373  algcvgblem  16732  isirred2  20631  isdomn3  20946  ist0-3  23643  mdegleb  26362  dchrelbas4  27552  toslublem  33515  tosglblem  33517  bj-exexalal  37446  bj-alcomexcom  37550  poimirlem25  38531  poimirlem30  38536  tsbi3  39035  ntrneikb  45053  fulltermc  50563  aacllem  50883