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  1049  ifpdfbi  1070  r19.23v  3180  raldifsni  4799  dff14a  7289  weniso  7373  dfom2  7888  dfsup2  9481  wemapsolem  9587  pwfseqlem3  10697  indstr  12955  rpnnen2lem12  16257  algcvgblem  16610  isirred2  20437  isdomn2OLD  20728  isdomn3  20731  ist0-3  23368  mdegleb  26117  dchrelbas4  27301  toslublem  32946  tosglblem  32948  bj-alcomexcom  36662  poimirlem25  37631  poimirlem30  37636  tsbi3  38121  ntrneikb  44083  aacllem  49031
  Copyright terms: Public domain W3C validator