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

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
StepHypRef Expression
1 con3 153 . 2 ((𝜑𝜓) → (¬ 𝜓 → ¬ 𝜑))
2 con4 113 . 2 ((¬ 𝜓 → ¬ 𝜑) → (𝜑𝜓))
31, 2impbii 209 1 ((𝜑𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
Colors of variables: wff setvar class
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  3183  raldifsni  4795  dff14a  7290  weniso  7374  dfom2  7889  dfsup2  9484  wemapsolem  9590  pwfseqlem3  10700  indstr  12958  rpnnen2lem12  16261  algcvgblem  16614  isirred2  20421  isdomn2OLD  20712  isdomn3  20715  ist0-3  23353  mdegleb  26103  dchrelbas4  27287  toslublem  32962  tosglblem  32964  bj-alcomexcom  36681  poimirlem25  37652  poimirlem30  37657  tsbi3  38142  ntrneikb  44107  fulltermc  49143  aacllem  49320
  Copyright terms: Public domain W3C validator