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

Theorem pm4.56 984
 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 979 . 2 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
21bicomi 225 1 ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 207   ∧ wa 396   ∨ wo 843 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  df-an 397  df-or 844 This theorem is referenced by:  oran  985  nornotOLD  1518  neanior  3114  prneimg  4784  ssxr  10704  isirred2  19387  aaliou3lem9  24873  mideulem2  26453  opphllem  26454  bj-dfbi4  33809  topdifinffinlem  34516  icorempo  34520  dalawlem13  36905  cdleme22b  37363  negn0nposznnd  39052  jm2.26lem3  39482  wopprc  39511  iunconnlem2  41153  icccncfext  42054  cncfiooicc  42061  fourierdlem25  42302  fourierdlem35  42312  fourierswlem  42400  fouriersw  42401  etransclem44  42448  sge0split  42576  islininds2  44441  digexp  44569
 Copyright terms: Public domain W3C validator