MPE Home 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  601  dfbi3  1018  19.23t  2117  19.23tOLD  2254  r19.23v  3052  raldifsni  4357  dff14a  6567  weniso  6644  dfom2  7109  dfsup2  8391  wemapsolem  8496  pwfseqlem3  9520  indstr  11794  rpnnen2lem12  14998  algcvgblem  15337  isirred2  18747  isdomn2  19347  ist0-3  21197  mdegleb  23869  dchrelbas4  25013  toslublem  29795  tosglblem  29797  poimirlem25  33564  poimirlem30  33569  tsbi3  34072  isdomn3  38099  ntrneikb  38709  conss34OLD  38963  aacllem  42875
  Copyright terms: Public domain W3C validator