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 1398) and the constant false (df-fal 1401), we will be able to prove these truth table values: (truantru 1419), (truanfal 1420), (falantru 1421), and (falanfal 1422).

Contrast with \/ (df-or 370), -> (wi 4), -/\ (df-nan 1344), and \/_ (df-xor 1364) . (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  1925  sban  2140  r19.35  3004  dfac5lem4  8528  kmlem3  8553  axrepprim  29074  axunprim  29075  axregprim  29077  axinfprim  29078  axacprim  29079  pm11.52  31292  dfxor4  37789
  Copyright terms: Public domain W3C validator