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

Definition df-an 371
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 1372) and the constant false (df-fal 1375), we will be able to prove these truth table values: (truantru 1393), (truanfal 1394), (falantru 1395), and (falanfal 1396).

Contrast with \/ (df-or 370), -> (wi 4), -/\ (df-nan 1334), and \/_ (df-xor 1351) . (Contributed by NM, 5-Jan-1993.)

Assertion
Ref Expression
df-an

Detailed syntax breakdown of Definition df-an
StepHypRef Expression
1 wph . . 3
2 wps . . 3
31, 2wa 369 . 2
42wn 3 . . . 4
51, 4wi 4 . . 3
65wn 3 . 2
73, 6wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  pm4.63  421  imnan  422  imp  429  ex  434  pm4.54  493  dfbi2  628  pm5.32  636  nfand  1858  sban  2091  r19.35  2867  dfac5lem4  8296  kmlem3  8321  axrepprim  27353  axunprim  27354  axregprim  27356  axinfprim  27357  axacprim  27358  pm11.52  29639
  Copyright terms: Public domain W3C validator