Theorem con34b 316

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

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

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 207

This theorem is referenced by:  mtt  364  pm4.14  806  dfbi3  1049  ifpdfbi  1070  r19.23v  3163  raldifsni  4751  dff14a  7216  weniso  7300  dfom2  7810  dfsup2  9347  wemapsolem  9455  pwfseqlem3  10571  indstr  12829  rpnnen2lem12  16150  algcvgblem  16504  isirred2  20357  isdomn2OLD  20645  isdomn3  20648  ist0-3  23289  mdegleb  26025  dchrelbas4  27210  toslublem  33054  tosglblem  33056  bj-alcomexcom  36881  poimirlem25  37842  poimirlem30  37847  tsbi3  38332  ntrneikb  44331  fulltermc  49752  aacllem  50042