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 . After we define the constant true (df-tru 1338) and the constant false (df-fal 1339), we will be able to prove these truth table values: (truantru 1355), (truanfal 1356), (falantru 1357), and (falanfal 1358).

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

Assertion
Ref Expression
df-an

Detailed syntax breakdown of Definition df-an
StepHypRef Expression
1 wph . . 3
2 wps . . 3
31, 2wa 360 . 2
42wn 3 . . . 4
51, 4wi 4 . . 3
65wn 3 . 2
73, 6wb 178 1
Colors of variables: wff set class
This definition is referenced by:  pm4.63  412  imnan  413  imp  420  ex  425  pm4.54  481  dfbi2  611  pm5.32  619  nfand  1847  nfanOLD  1852  hbanOLD  1855  equsexOLD  2010  sban  2149  r19.35  2910  dfac5lem4  8178  kmlem3  8203  axrepprim  26493  axunprim  26494  axregprim  26496  axinfprim  26497  axacprim  26498  pm11.52  28813  equsexNEW11  31042  sbanNEW11  31121
  Copyright terms: Public domain W3C validator