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

Theorem con34b 317
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 210 1 ((𝜑𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207
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 208
This theorem is referenced by:  mtt  366  pm4.14  803  dfbi3  1043  r19.23v  3284  raldifsni  4727  dff14a  7022  weniso  7099  dfom2  7570  dfsup2  8897  wemapsolem  9003  pwfseqlem3  10071  indstr  12305  rpnnen2lem12  15568  algcvgblem  15911  isirred2  19371  isdomn2  19991  ist0-3  21872  mdegleb  24576  dchrelbas4  25736  toslublem  30571  tosglblem  30573  poimirlem25  34787  poimirlem30  34792  tsbi3  35284  isdomn3  39672  ntrneikb  40312  aacllem  44737
  Copyright terms: Public domain W3C validator