MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3ianor 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  3899  fr3nr  4719  funtpg  5460  bropopvvv  6385  elfznelfzo  11147  hashtpg  11646  spthispth  21526  lpni  21720  xrdifh  24096  dvreasin  26179  2wlkonot3v  28072  2spthonot3v  28073  2spotdisj  28164
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