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  3189  raldifsni  4754  dff14a  7274  weniso  7364  dfom2  7879  dfsup2  9439  wemapsolem  9547  pwfseqlem3  10748  indstr  13046  rpnnen2lem12  16398  algcvgblem  16757  isirred2  20656  isdomn3  20971  ist0-3  23668  mdegleb  26387  dchrelbas4  27575  toslublem  33579  tosglblem  33581  bj-exexalal  37568  bj-alcomexcom  37672  poimirlem25  38656  poimirlem30  38661  tsbi3  39160  ntrneikb  45187  fulltermc  50739  aacllem  51107