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  3024  prneimg  4532  ordtri3OLD  5921  ssxr  10319  isirred2  18921  aaliou3lem9  24324  mideulem2  25846  opphllem  25847  bj-dfbi4  32886  topdifinffinlem  33524  icorempt2  33528  dalawlem13  35690  cdleme22b  36149  jm2.26lem3  38088  wopprc  38117  iunconnlem2  39688  icccncfext  40621  cncfiooicc  40628  fourierdlem25  40870  fourierdlem35  40880  fourierswlem  40968  fouriersw  40969  etransclem44  41016  sge0split  41147  islininds2  42801  digexp  42929
  Copyright terms: Public domain W3C validator