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

Definition df-an 364
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 1355) and the constant false (df-fal 1356), we will be able to prove these truth table values: (truantru 1372), (truanfal 1373), (falantru 1374), and (falanfal 1375).

Contrast with \/ (df-or 363), -> (wi 4), -/\ (df-nan 1319), and \/_ (df-xor 1336) . (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 362 . 2
42wn 3 . . . 4
51, 4wi 4 . . 3
65wn 3 . 2
73, 6wb 178 1
Colors of variables: wff setvar class
This definition is referenced by:  pm4.63  414  imnan  415  imp  422  ex  427  pm4.54  483  dfbi2  613  pm5.32  621  nfand  1848  sban  2081  r19.35  2846  dfac5lem4  8243  kmlem3  8268  axrepprim  27055  axunprim  27056  axregprim  27058  axinfprim  27059  axacprim  27060  pm11.52  29312
  Copyright terms: Public domain W3C validator