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

Contrast with (df-or 384), (wi 4), (df-nan 1440), and (df-xor 1457) . (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 195 1 wff ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  pm4.63  436  imnan  437  imp  444  ex  449  pm4.54  513  dfbi2  658  pm5.32  666  nfand  1814  nfanOLD  1817  nfan1  2056  nfandOLD  2220  sban  2387  r19.35  3065  dfac5lem4  8832  kmlem3  8857  axrepprim  30833  axunprim  30834  axregprim  30836  axinfprim  30837  axacprim  30838  dfxor4  37077  df3an2  37080  pm11.52  37608
  Copyright terms: Public domain W3C validator