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 380
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 1471) and the constant false (df-fal 1474), we will be able to prove these truth table values: ((⊤ ∧ ⊤) ↔ ⊤) (truantru 1490), ((⊤ ∧ ⊥) ↔ ⊥) (truanfal 1491), ((⊥ ∧ ⊤) ↔ ⊥) (falantru 1492), and ((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1493).

Contrast with (df-or 379), (wi 4), (df-nan 1429), and (df-xor 1447) . (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 378 . 2 wff (𝜑𝜓)
42wn 3 . . . 4 wff ¬ 𝜓
51, 4wi 4 . . 3 wff (𝜑 → ¬ 𝜓)
65wn 3 . 2 wff ¬ (𝜑 → ¬ 𝜓)
73, 6wb 191 1 wff ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  pm4.63  430  imnan  431  imp  438  ex  443  pm4.54  507  dfbi2  649  pm5.32  657  nfand  2061  sban  2282  r19.35  2958  dfac5lem4  8642  kmlem3  8667  axrepprim  30481  axunprim  30482  axregprim  30484  axinfprim  30485  axacprim  30486  dfxor4  36597  df3an2  36600  pm11.52  37093
  Copyright terms: Public domain W3C validator