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

Theorem pm4.56 1012
Description: Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
Assertion
Ref Expression
pm4.56 ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))

Proof of Theorem pm4.56
StepHypRef Expression
1 ioran 1007 . 2 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
21bicomi 216 1 ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 198  wa 385  wo 874
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 199  df-an 386  df-or 875
This theorem is referenced by:  oran  1013  neanior  3061  prneimg  4571  ssxr  10395  isirred2  19014  aaliou3lem9  24443  mideulem2  25975  opphllem  25976  bj-dfbi4  33054  topdifinffinlem  33685  icorempt2  33689  dalawlem13  35896  cdleme22b  36354  jm2.26lem3  38341  wopprc  38370  iunconnlem2  39919  icccncfext  40832  cncfiooicc  40839  fourierdlem25  41080  fourierdlem35  41090  fourierswlem  41178  fouriersw  41179  etransclem44  41226  sge0split  41357  islininds2  43060  digexp  43188
  Copyright terms: Public domain W3C validator