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

Contrast with \/ (df-or 370), -> (wi 4), -/\ (df-nan 1335), and \/_ (df-xor 1352) . (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  1863  sban  2101  r19.35  2976  dfac5lem4  8433  kmlem3  8458  axrepprim  27809  axunprim  27810  axregprim  27812  axinfprim  27813  axacprim  27814  pm11.52  30099
  Copyright terms: Public domain W3C validator