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 395
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 1536) and the constant false (df-fal 1546), we will be able to prove these truth table values: ((⊤ ∧ ⊤) ↔ ⊤) (truantru 1566), ((⊤ ∧ ⊥) ↔ ⊥) (truanfal 1567), ((⊥ ∧ ⊤) ↔ ⊥) (falantru 1568), and ((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1569).

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 846), (wi 4), (df-nan 1485), and (df-xor 1505). (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 394 . 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  396  imnan  398  imp  405  ex  411  dfbi2  473  pm5.32  572  pm4.54  984  nfand  1892  nfan1  2188  dfac5lem4  10151  kmlem3  10177  nolt02o  27674  axrepprim  35427  axunprim  35428  axregprim  35430  axinfprim  35431  axacprim  35432  aks6d1c6lem3  41775  orddif0suc  42839  dfxor4  43338  df3an2  43341  expandan  43867  ismnuprim  43873  pm11.52  43966
  Copyright terms: Public domain W3C validator