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 517
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 512 . 2 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
21bicomi 214 1 ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  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 197  df-or 384  df-an 385
This theorem is referenced by:  oran  518  neanior  3016  prneimg  4524  ordtri3OLD  5913  ssxr  10291  isirred2  18893  aaliou3lem9  24296  mideulem2  25817  opphllem  25818  bj-dfbi4  32856  topdifinffinlem  33498  icorempt2  33502  dalawlem13  35664  cdleme22b  36123  jm2.26lem3  38062  wopprc  38091  iunconnlem2  39662  icccncfext  40595  cncfiooicc  40602  fourierdlem25  40844  fourierdlem35  40854  fourierswlem  40942  fouriersw  40943  etransclem44  40990  sge0split  41121  islininds2  42775  digexp  42903
  Copyright terms: Public domain W3C validator