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 516
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 511 . 2 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
21bicomi 214 1 ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wo 383  wa 384
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 197  df-or 385  df-an 386
This theorem is referenced by:  oran  517  neanior  2882  prneimg  4363  ordtri3OLD  5729  ssxr  10067  isirred2  18641  aaliou3lem9  24043  mideulem2  25560  opphllem  25561  bj-dfbi4  32253  topdifinffinlem  32866  icorempt2  32870  dalawlem13  34688  cdleme22b  35148  jm2.26lem3  37087  wopprc  37116  iunconnlem2  38693  icccncfext  39435  cncfiooicc  39442  fourierdlem25  39686  fourierdlem35  39696  fourierswlem  39784  fouriersw  39785  etransclem44  39832  sge0split  39963  islininds2  41591  digexp  41723
  Copyright terms: Public domain W3C validator