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 385
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 1623) and the constant false (df-fal 1626), we will be able to prove these truth table values: ((⊤ ∧ ⊤) ↔ ⊤) (truantru 1643), ((⊤ ∧ ⊥) ↔ ⊥) (truanfal 1644), ((⊥ ∧ ⊤) ↔ ⊥) (falantru 1645), and ((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1646).

Contrast with (df-or 384), (wi 4), (df-nan 1585), and (df-xor 1602) . (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 383 . 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  436  imnan  437  imp  444  ex  449  pm4.54  515  dfbi2  663  pm5.32  671  nfand  1963  nfanOLD  1966  nfan1  2203  nfandOLD  2365  sban  2524  r19.35  3210  dfac5lem4  9110  kmlem3  9137  axrepprim  31857  axunprim  31858  axregprim  31860  axinfprim  31861  axacprim  31862  nolt02o  32122  dfxor4  38529  df3an2  38532  pm11.52  39057
  Copyright terms: Public domain W3C validator