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  1852  sban  1961  r19.35  2649  dfac5lem4  7637  kmlem3  7662  axrepprim  23219  axunprim  23220  axregprim  23222  axinfprim  23223  axacprim  23224  pm11.52  26751  ax10lem17X  27887  equsexv-x12  27914  ax9lem10  27950
  Copyright terms: Public domain W3C validator