Theorem pm4.56 516

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

Assertion

Ref	Expression
pm4.56	|- ( ( -. ph /\ -. ps ) <-> -. ( ph \/ ps ) )

Proof of Theorem pm4.56

Step	Hyp	Ref	Expression
1		ioran 511	. 2 |- ( -. ( ph \/ ps ) <-> ( -. ph /\ -. ps ) )
2	1	bicomi 214	1 |- ( ( -. ph /\ -. ps ) <-> -. ( ph \/ ps ) )

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  2886  prneimg  4388  ordtri3OLD  5760  ssxr  10107  isirred2  18701  aaliou3lem9  24105  mideulem2  25626  opphllem  25627  bj-dfbi4  32558  topdifinffinlem  33195  icorempt2  33199  dalawlem13  35169  cdleme22b  35629  jm2.26lem3  37568  wopprc  37597  iunconnlem2  39171  icccncfext  40100  cncfiooicc  40107  fourierdlem25  40349  fourierdlem35  40359  fourierswlem  40447  fouriersw  40448  etransclem44  40495  sge0split  40626  islininds2  42273  digexp  42401