Theorem con34b 316

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 153	. 2 ⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))
2		con4 113	. 2 ⊢ ((¬ 𝜓 → ¬ 𝜑) → (𝜑 → 𝜓))
3	1, 2	impbii 209	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))

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

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 207

This theorem is referenced by:  mtt  364  pm4.14  806  dfbi3  1049  ifpdfbi  1070  r19.23v  3159  raldifsni  4747  dff14a  7204  weniso  7288  dfom2  7798  dfsup2  9328  wemapsolem  9436  pwfseqlem3  10548  indstr  12811  rpnnen2lem12  16131  algcvgblem  16485  isirred2  20337  isdomn2OLD  20625  isdomn3  20628  ist0-3  23258  mdegleb  25994  dchrelbas4  27179  toslublem  32948  tosglblem  32950  bj-alcomexcom  36713  poimirlem25  37684  poimirlem30  37689  tsbi3  38174  ntrneikb  44126  fulltermc  49542  aacllem  49832