MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm4.56 Structured version   Unicode version

Theorem pm4.56 493
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
StepHypRef Expression
1 ioran 488 . 2  |-  ( -.  ( ph  \/  ps ) 
<->  ( -.  ph  /\  -.  ps ) )
21bicomi 202 1  |-  ( ( -.  ph  /\  -.  ps ) 
<->  -.  ( ph  \/  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    \/ wo 366    /\ wa 367
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 185  df-or 368  df-an 369
This theorem is referenced by:  oran  494  neanior  2728  prneimg  4153  ordtri3  5446  ssxr  9685  isirred2  17670  aaliou3lem9  23038  coltr2  24413  mideulem2  24494  opphllem  24495  bj-dfbi4  30720  topdifinffinlem  31264  icorempt2  31268  dalawlem13  32900  cdleme22b  33360  jm2.26lem3  35305  wopprc  35334  iunconlem2  36766  icccncfext  37058  cncfiooicc  37065  fourierdlem25  37282  fourierdlem35  37292  fourierswlem  37381  fouriersw  37382  etransclem44  37429  islininds2  38596  digexp  38738
  Copyright terms: Public domain W3C validator