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

Definition df-an 362
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 1315) and the constant false  F. (df-fal 1316), we will be able to prove these truth table values:  ( (  T.  /\  T.  )  <->  T.  ) (truantru 1332), 
( (  T.  /\  F.  )  <->  F.  ) (truanfal 1333),  ( (  F.  /\  T.  )  <->  F.  ) (falantru 1334), and  ( (  F.  /\  F.  )  <->  F.  ) (falanfal 1335).

Contrast with  \/ (df-or 361), 
-> (wi 6),  -/\ (df-nan 1293), and  \/_ (df-xor 1301) . (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 360 . 2  wff  ( ph  /\ 
ps )
42wn 5 . . . 4  wff  -.  ps
51, 4wi 6 . . 3  wff  ( ph  ->  -.  ps )
65wn 5 . 2  wff  -.  ( ph  ->  -.  ps )
73, 6wb 178 1  wff  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
Colors of variables: wff set class
This definition is referenced by:  pm4.63  412  imnan  413  imp  420  ex  425  pm4.54  481  dfbi2  612  pm5.32  620  ax10lem17  1666  hban  1724  nfand  1729  nfan  1737  equsex  1853  sban  1962  r19.35  2660  dfac5lem4  7707  kmlem3  7732  axrepprim  23406  axunprim  23407  axregprim  23409  axinfprim  23410  axacprim  23411  pm11.52  26938  ax10lem17X  28237  equsexv-x12  28264  ax9lem10  28300
  Copyright terms: Public domain W3C validator