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  2658  dfac5lem4  7686  kmlem3  7711  axrepprim  23385  axunprim  23386  axregprim  23388  axinfprim  23389  axacprim  23390  pm11.52  26917  ax10lem17X  28216  equsexv-x12  28243  ax9lem10  28279
  Copyright terms: Public domain W3C validator