Theorem pm4.56 988

Description: Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)

Assertion

Ref	Expression
pm4.56	⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))

Proof of Theorem pm4.56

Step	Hyp	Ref	Expression
1		ioran 983	. 2 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
2	1	bicomi 227	1 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   ∨ wo 846

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 210  df-an 400  df-or 847

This theorem is referenced by:  oran  989  nornotOLD  1530  neanior  3027  rexprg  4588  prneimg  4741  unfi  8774  ssxr  10791  isirred2  19576  aaliou3lem9  25101  mideulem2  26683  opphllem  26684  bj-dfbi4  34400  topdifinffinlem  35164  icorempo  35168  dalawlem13  37543  cdleme22b  38001  metakunt1  39739  negn0nposznnd  39909  jm2.26lem3  40418  wopprc  40447  iunconnlem2  42116  icccncfext  42993  cncfiooicc  43000  fourierdlem25  43238  fourierdlem35  43248  fourierswlem  43336  fouriersw  43337  etransclem44  43384  sge0split  43512  islininds2  45389  digexp  45517