NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-an Unicode version

Definition df-an 360
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 (2 = 2 3 = 3). After we define the constant true (df-tru 1319) and the constant false (df-fal 1320), we will be able to prove these truth table values: (truantru 1336), (truanfal 1337), (falantru 1338), and (falanfal 1339).

Contrast with (df-or 359), (wi 4), (df-nan 1288), and  \/_ (df-xor 1305) . (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 358 . 2
42wn 3 . . . 4
51, 4wi 4 . . 3
65wn 3 . 2
73, 6wb 176 1
Colors of variables: wff setvar class
This definition is referenced by:  pm4.63  410  imnan  411  imp  418  ex  423  pm4.54  479  dfbi2  609  pm5.32  617  nfand  1822  nfanOLD  1826  hbanOLD  1829  equsex  1962  sban  2069  r19.35  2758  disj  3591
  Copyright terms: Public domain W3C validator