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  3191  raldifsni  4761  dff14a  7271  weniso  7361  dfom2  7868  dfsup2  9418  wemapsolem  9526  pwfseqlem3  10673  indstr  12969  rpnnen2lem12  16319  algcvgblem  16673  isirred2  20568  isdomn3  20882  ist0-3  23576  mdegleb  26296  dchrelbas4  27487  toslublem  33420  tosglblem  33422  bj-exexalal  37315  bj-alcomexcom  37419  poimirlem25  38402  poimirlem30  38407  tsbi3  38891  ntrneikb  44942  fulltermc  50445  aacllem  50780