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 397
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 1542) and the constant false (df-fal 1552), we will be able to prove these truth table values: ((⊤ ∧ ⊤) ↔ ⊤) (truantru 1572), ((⊤ ∧ ⊥) ↔ ⊥) (truanfal 1573), ((⊥ ∧ ⊤) ↔ ⊥) (falantru 1574), and ((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1575).

This is our first use of the biconditional connective in a definition; we use the biconditional connective in place of the traditional "<=def=>", which means the same thing, except that we can manipulate the biconditional connective directly in proofs rather than having to rely on an informal definition substitution rule. Note that if we mechanically substitute ¬ (𝜑 → ¬ 𝜓) for (𝜑𝜓), we end up with an instance of previously proved theorem biid 260. This is the justification for the definition, along with the fact that it introduces a new symbol . Contrast with (df-or 845), (wi 4), (df-nan 1487), and (df-xor 1507). (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 396 . 2 wff (𝜑𝜓)
42wn 3 . . . 4 wff ¬ 𝜓
51, 4wi 4 . . 3 wff (𝜑 → ¬ 𝜓)
65wn 3 . 2 wff ¬ (𝜑 → ¬ 𝜓)
73, 6wb 205 1 wff ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  pm4.63  398  imnan  400  imp  407  ex  413  dfbi2  475  pm5.32  574  pm4.54  984  nfand  1900  nfan1  2193  dfac5lem4  9880  kmlem3  9906  axrepprim  33640  axunprim  33641  axregprim  33643  axinfprim  33644  axacprim  33645  nolt02o  33895  dfxor4  41344  df3an2  41347  expandan  41876  ismnuprim  41882  pm11.52  41975
  Copyright terms: Public domain W3C validator