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

Theorem con34b 305
 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 149 . 2 ((𝜑𝜓) → (¬ 𝜓 → ¬ 𝜑))
2 con4 112 . 2 ((¬ 𝜓 → ¬ 𝜑) → (𝜑𝜓))
31, 2impbii 199 1 ((𝜑𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196 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 197 This theorem is referenced by:  mtt  353  pm4.14  603  dfbi3  1036  19.23t  2226  19.23tOLD  2363  r19.23v  3161  raldifsni  4470  dff14a  6690  weniso  6767  dfom2  7232  dfsup2  8515  wemapsolem  8620  pwfseqlem3  9674  indstr  11949  rpnnen2lem12  15153  algcvgblem  15492  isirred2  18901  isdomn2  19501  ist0-3  21351  mdegleb  24023  dchrelbas4  25167  toslublem  29976  tosglblem  29978  poimirlem25  33747  poimirlem30  33752  tsbi3  34255  isdomn3  38284  ntrneikb  38894  conss34OLD  39148  aacllem  43060
 Copyright terms: Public domain W3C validator