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

Definition df-an 386
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 1484) and the constant false (df-fal 1487), we will be able to prove these truth table values: ((⊤ ∧ ⊤) ↔ ⊤) (truantru 1504), ((⊤ ∧ ⊥) ↔ ⊥) (truanfal 1505), ((⊥ ∧ ⊤) ↔ ⊥) (falantru 1506), and ((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1507).

Contrast with (df-or 385), (wi 4), (df-nan 1446), and (df-xor 1463) . (Contributed by NM, 5-Jan-1993.)

Assertion
Ref Expression
df-an ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))

Detailed syntax breakdown of Definition df-an
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
31, 2wa 384 . 2 wff (𝜑𝜓)
42wn 3 . . . 4 wff ¬ 𝜓
51, 4wi 4 . . 3 wff (𝜑 → ¬ 𝜓)
65wn 3 . 2 wff ¬ (𝜑 → ¬ 𝜓)
73, 6wb 196 1 wff ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  pm4.63  437  imnan  438  imp  445  ex  450  pm4.54  514  dfbi2  659  pm5.32  667  nfand  1824  nfanOLD  1827  nfan1  2066  nfandOLD  2230  sban  2397  r19.35  3079  dfac5lem4  8934  kmlem3  8959  axrepprim  31553  axunprim  31554  axregprim  31556  axinfprim  31557  axacprim  31558  nolt02o  31819  dfxor4  37877  df3an2  37880  pm11.52  38406
  Copyright terms: Public domain W3C validator