MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con34b Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 con3 156 . 2 ((𝜑𝜓) → (¬ 𝜓 → ¬ 𝜑))
2 con4 113 . 2 ((¬ 𝜓 → ¬ 𝜑) → (𝜑𝜓))
31, 2impbii 212 1 ((𝜑𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209
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 210
This theorem is referenced by:  mtt  368  pm4.14  807  dfbi3  1050  ifpdfbi  1071  r19.23v  3198  raldifsni  4708  dff14a  7082  weniso  7163  dfom2  7646  dfsup2  9060  wemapsolem  9166  pwfseqlem3  10274  indstr  12512  rpnnen2lem12  15786  algcvgblem  16134  isirred2  19719  isdomn2  20337  ist0-3  22242  mdegleb  24962  dchrelbas4  26124  toslublem  30969  tosglblem  30971  poimirlem25  35539  poimirlem30  35544  tsbi3  36030  isdomn3  40732  ntrneikb  41381  aacllem  46176
  Copyright terms: Public domain W3C validator