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  2888  prneimg  4361  ordtri3OLD  5722  ssxr  10052  isirred2  18617  aaliou3lem9  24004  mideulem2  25521  opphllem  25522  bj-dfbi4  32192  topdifinffinlem  32819  icorempt2  32823  dalawlem13  34635  cdleme22b  35095  jm2.26lem3  37034  wopprc  37063  iunconnlem2  38640  icccncfext  39391  cncfiooicc  39398  fourierdlem25  39643  fourierdlem35  39653  fourierswlem  39741  fouriersw  39742  etransclem44  39789  sge0split  39920  islininds2  41535  digexp  41667
  Copyright terms: Public domain W3C validator