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

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

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 210

This theorem is referenced by:  mtt  367  pm4.14  818  dfbi3  1063  ifpdfbiOLD  1085  r19.23v  3192  raldifsni  4758  dff14a  7258  weniso  7342  dfom2  7852  dfsup2  9392  wemapsolem  9500  pwfseqlem3  10633  indstr  12931  rpnnen2lem12  16271  algcvgblem  16625  isirred2  20494  isdomn3  20790  ist0-3  23463  mdegleb  26182  dchrelbas4  27365  toslublem  33205  tosglblem  33207  bj-exexalal  37061  bj-alcomexcom  37165  poimirlem25  38156  poimirlem30  38161  tsbi3  38646  ntrneikb  44682  fulltermc  50140  aacllem  50430