MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-an Structured version   Unicode version

Definition df-an 361
Description: Define conjunction (logical 'and'). Definition of [Margaris] p. 49. When both the left and right operand are true, the result is true; when either is false, the result is false. For example, it is true that  ( 2  =  2  /\  3  =  3 ). After we define the constant true  T. (df-tru 1328) and the constant false  F. (df-fal 1329), we will be able to prove these truth table values:  ( (  T.  /\  T.  )  <->  T.  ) (truantru 1345), 
( (  T.  /\  F.  )  <->  F.  ) (truanfal 1346),  ( (  F.  /\  T.  )  <->  F.  ) (falantru 1347), and  ( (  F.  /\  F.  )  <->  F.  ) (falanfal 1348).

Contrast with  \/ (df-or 360), 
-> (wi 4),  -/\ (df-nan 1297), and  \/_ (df-xor 1314) . (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
df-an  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )

Detailed syntax breakdown of Definition df-an
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
31, 2wa 359 . 2  wff  ( ph  /\ 
ps )
42wn 3 . . . 4  wff  -.  ps
51, 4wi 4 . . 3  wff  ( ph  ->  -.  ps )
65wn 3 . 2  wff  -.  ( ph  ->  -.  ps )
73, 6wb 177 1  wff  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
Colors of variables: wff set class
This definition is referenced by:  pm4.63  411  imnan  412  imp  419  ex  424  pm4.54  480  dfbi2  610  pm5.32  618  nfand  1843  nfanOLD  1848  hbanOLD  1851  equsexOLD  2003  sban  2143  r19.35  2847  dfac5lem4  7999  kmlem3  8024  axrepprim  25143  axunprim  25144  axregprim  25146  axinfprim  25147  axacprim  25148  pm11.52  27553  equsexNEW7  29427  sbanNEW7  29506
  Copyright terms: Public domain W3C validator