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

Theorem 3ianor 951
Description: Negated triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.)
Assertion
Ref Expression
3ianor  |-  ( -.  ( ph  /\  ps  /\ 
ch )  <->  ( -.  ph  \/  -.  ps  \/  -.  ch ) )

Proof of Theorem 3ianor
StepHypRef Expression
1 3anor 950 . . 3  |-  ( (
ph  /\  ps  /\  ch ) 
<->  -.  ( -.  ph  \/  -.  ps  \/  -.  ch ) )
21con2bii 323 . 2  |-  ( ( -.  ph  \/  -.  ps  \/  -.  ch )  <->  -.  ( ph  /\  ps  /\ 
ch ) )
32bicomi 194 1  |-  ( -.  ( ph  /\  ps  /\ 
ch )  <->  ( -.  ph  \/  -.  ps  \/  -.  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177    \/ w3o 935    /\ w3a 936
This theorem is referenced by:  tppreqb  3931  fr3nr  4752  funtpg  5493  bropopvvv  6418  elfznelfzo  11182  hashtpg  11681  spthispth  21563  lpni  21757  xrdifh  24133  dvreasin  26243  wrdsymb0  28111  lswrd0  28191  2wlkonot3v  28259  2spthonot3v  28260  2spotdisj  28351
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938
  Copyright terms: Public domain W3C validator