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

Theorem pm4.56 515
 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 510 . 2 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
21bicomi 213 1 ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195   ∨ wo 382   ∧ wa 383 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 196  df-or 384  df-an 385 This theorem is referenced by:  oran  516  neanior  2874  prneimg  4328  ordtri3OLD  5677  ssxr  9986  isirred2  18524  aaliou3lem9  23909  mideulem2  25426  opphllem  25427  bj-dfbi4  31728  topdifinffinlem  32371  icorempt2  32375  dalawlem13  34187  cdleme22b  34647  jm2.26lem3  36586  wopprc  36615  iunconlem2  38193  icccncfext  38773  cncfiooicc  38780  fourierdlem25  39025  fourierdlem35  39035  fourierswlem  39123  fouriersw  39124  etransclem44  39171  sge0split  39302  islininds2  42067  digexp  42199
 Copyright terms: Public domain W3C validator