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

Contrast with (df-or 385), (wi 4), (df-nan 1445), and (df-xor 1462) . (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  1823  nfanOLD  1826  nfan1  2066  nfandOLD  2231  sban  2398  r19.35  3076  dfac5lem4  8893  kmlem3  8918  axrepprim  31284  axunprim  31285  axregprim  31287  axinfprim  31288  axacprim  31289  dfxor4  37536  df3an2  37539  pm11.52  38065
  Copyright terms: Public domain W3C validator