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

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 261. This is the justification for the definition, along with the fact that it introduces a new symbol . Contrast with (df-or 847), (wi 4), (df-nan 1486), and (df-xor 1506). (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 395 . 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  397  imnan  399  imp  406  ex  412  dfbi2  474  pm5.32  573  pm4.54  985  nfand  1893  nfan1  2189  dfac5lem4  10150  kmlem3  10176  nolt02o  27641  axrepprim  35296  axunprim  35297  axregprim  35299  axinfprim  35300  axacprim  35301  aks6d1c6lem3  41644  orddif0suc  42697  dfxor4  43196  df3an2  43199  expandan  43725  ismnuprim  43731  pm11.52  43824
  Copyright terms: Public domain W3C validator