Theorem con34b 315

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

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

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 206

This theorem is referenced by:  mtt  363  pm4.14  803  dfbi3  1046  ifpdfbi  1067  r19.23v  3180  raldifsni  4799  dff14a  7273  weniso  7355  dfom2  7861  dfsup2  9443  wemapsolem  9549  pwfseqlem3  10659  indstr  12906  rpnnen2lem12  16174  algcvgblem  16520  isirred2  20314  isdomn2  21117  ist0-3  23071  mdegleb  25816  dchrelbas4  26980  toslublem  32407  tosglblem  32409  bj-alcomexcom  35863  poimirlem25  36818  poimirlem30  36823  tsbi3  37308  isdomn3  42250  ntrneikb  43149  aacllem  47937