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  807  dfbi3  1050  ifpdfbi  1071  r19.23v  3165  raldifsni  4739  dff14a  7218  weniso  7302  dfom2  7812  dfsup2  9350  wemapsolem  9458  pwfseqlem3  10574  indstr  12857  rpnnen2lem12  16183  algcvgblem  16537  isirred2  20392  isdomn2OLD  20680  isdomn3  20683  ist0-3  23320  mdegleb  26039  dchrelbas4  27220  toslublem  33047  tosglblem  33049  bj-exexalal  36887  bj-alcomexcom  36991  poimirlem25  37980  poimirlem30  37985  tsbi3  38470  ntrneikb  44539  fulltermc  49998  aacllem  50288