Theorem con34b 318

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

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

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 209

This theorem is referenced by:  mtt  367  pm4.14  805  dfbi3  1044  r19.23v  3281  raldifsni  4730  dff14a  7030  weniso  7109  dfom2  7584  dfsup2  8910  wemapsolem  9016  pwfseqlem3  10084  indstr  12319  rpnnen2lem12  15580  algcvgblem  15923  isirred2  19453  isdomn2  20074  ist0-3  21955  mdegleb  24660  dchrelbas4  25821  toslublem  30656  tosglblem  30658  poimirlem25  34919  poimirlem30  34924  tsbi3  35415  isdomn3  39811  ntrneikb  40451  aacllem  44909