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

Theorem con34b 304
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 147 . 2 ((𝜑𝜓) → (¬ 𝜓 → ¬ 𝜑))
2 con4 110 . 2 ((¬ 𝜓 → ¬ 𝜑) → (𝜑𝜓))
31, 2impbii 197 1 ((𝜑𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194
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 195
This theorem is referenced by:  mtt  352  pm4.14  599  19.23t  2065  19.23tOLD  2205  r19.23v  3004  raldifsni  4264  dff14a  6405  weniso  6482  dfom2  6936  dfsup2  8210  wemapsolem  8315  pwfseqlem3  9338  indstr  11588  rpnnen2lem12  14739  algcvgblem  15074  isirred2  18470  isdomn2  19066  ist0-3  20901  mdegleb  23545  dchrelbas4  24685  toslublem  28804  tosglblem  28806  poimirlem25  32400  poimirlem30  32405  tsbi3  32908  isdomn3  36597  ntrneikb  37208  conss34OLD  37463  aacllem  42312
  Copyright terms: Public domain W3C validator