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  3193  raldifsni  4758  dff14a  7300  weniso  7390  dfom2  7906  dfsup2  9466  wemapsolem  9574  pwfseqlem3  10775  indstr  13073  rpnnen2lem12  16425  algcvgblem  16784  isirred2  20684  isdomn3  20999  ist0-3  23696  mdegleb  26415  dchrelbas4  27603  toslublem  33606  tosglblem  33608  bj-exexalal  37667  bj-alcomexcom  37771  poimirlem25  38768  poimirlem30  38773  tsbi3  39270  ntrneikb  45297  fulltermc  50861  aacllem  51251