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 384
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 1477) and the constant false (df-fal 1480), we will be able to prove these truth table values: ((⊤ ∧ ⊤) ↔ ⊤) (truantru 1496), ((⊤ ∧ ⊥) ↔ ⊥) (truanfal 1497), ((⊥ ∧ ⊤) ↔ ⊥) (falantru 1498), and ((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1499).

Contrast with (df-or 383), (wi 4), (df-nan 1439), and (df-xor 1456) . (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 382 . 2 wff (𝜑𝜓)
42wn 3 . . . 4 wff ¬ 𝜓
51, 4wi 4 . . 3 wff (𝜑 → ¬ 𝜓)
65wn 3 . 2 wff ¬ (𝜑 → ¬ 𝜓)
73, 6wb 194 1 wff ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  pm4.63  435  imnan  436  imp  443  ex  448  pm4.54  512  dfbi2  657  pm5.32  665  nfand  1813  nfanOLD  1816  nfan1  2055  nfandOLD  2219  sban  2386  r19.35  3064  dfac5lem4  8809  kmlem3  8834  axrepprim  30639  axunprim  30640  axregprim  30642  axinfprim  30643  axacprim  30644  dfxor4  36873  df3an2  36876  pm11.52  37404
  Copyright terms: Public domain W3C validator