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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  mtt  367  pm4.14  819  dfbi3  1065  ifpdfbiOLD  1087  r19.23v  3195  raldifsni  4768  dff14a  7275  weniso  7365  dfom2  7873  dfsup2  9414  wemapsolem  9522  pwfseqlem3  10663  indstr  12958  rpnnen2lem12  16306  algcvgblem  16660  isirred2  20536  isdomn3  20850  ist0-3  23539  mdegleb  26258  dchrelbas4  27444  toslublem  33323  tosglblem  33325  bj-exexalal  37240  bj-alcomexcom  37344  poimirlem25  38337  poimirlem30  38342  tsbi3  38825  ntrneikb  44861  fulltermc  50330  aacllem  50662