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  3161  raldifsni  4759  dff14a  7245  weniso  7329  dfom2  7844  dfsup2  9395  wemapsolem  9503  pwfseqlem3  10613  indstr  12875  rpnnen2lem12  16193  algcvgblem  16547  isirred2  20330  isdomn2OLD  20621  isdomn3  20624  ist0-3  23232  mdegleb  25969  dchrelbas4  27154  toslublem  32898  tosglblem  32900  bj-alcomexcom  36668  poimirlem25  37639  poimirlem30  37644  tsbi3  38129  ntrneikb  44083  fulltermc  49500  aacllem  49790