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

Theorem con34b 307
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 150 . 2 ((𝜑𝜓) → (¬ 𝜓 → ¬ 𝜑))
2 con4 113 . 2 ((¬ 𝜓 → ¬ 𝜑) → (𝜑𝜓))
31, 2impbii 200 1 ((𝜑𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197
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 198
This theorem is referenced by:  mtt  355  pm4.14  841  dfbi3  1072  19.23tOLD  2243  r19.23v  3170  raldifsni  4482  dff14a  6721  weniso  6798  dfom2  7267  dfsup2  8559  wemapsolem  8664  pwfseqlem3  9737  indstr  11960  rpnnen2lem12  15239  algcvgblem  15574  isirred2  18971  isdomn2  19576  ist0-3  21432  mdegleb  24118  dchrelbas4  25262  toslublem  30117  tosglblem  30119  poimirlem25  33861  poimirlem30  33866  tsbi3  34366  isdomn3  38462  ntrneikb  39069  aacllem  43222
  Copyright terms: Public domain W3C validator