Theorem con34b 317

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

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

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 208

This theorem is referenced by:  mtt  365  pm4.14  812  dfbi3  1055  ifpdfbi  1076  r19.23v  3167  raldifsni  4735  dff14a  7221  weniso  7305  dfom2  7815  dfsup2  9354  wemapsolem  9462  pwfseqlem3  10581  indstr  12864  rpnnen2lem12  16190  algcvgblem  16544  isirred2  20399  isdomn2OLD  20691  isdomn3  20694  ist0-3  23335  mdegleb  26054  dchrelbas4  27231  toslublem  33058  tosglblem  33060  bj-exexalal  36924  bj-alcomexcom  37028  poimirlem25  38019  poimirlem30  38024  tsbi3  38509  ntrneikb  44545  fulltermc  50008  aacllem  50298