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 383
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 1634) and the constant false (df-fal 1637), we will be able to prove these truth table values: ((⊤ ∧ ⊤) ↔ ⊤) (truantru 1654), ((⊤ ∧ ⊥) ↔ ⊥) (truanfal 1655), ((⊥ ∧ ⊤) ↔ ⊥) (falantru 1656), and ((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1657).

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 251. This is the justification for the definition, along with the fact that it introduces a new symbol . Contrast with (df-or 837), (wi 4), (df-nan 1596), and (df-xor 1613) . (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 382 . 2 wff (𝜑𝜓)
42wn 3 . . . 4 wff ¬ 𝜓
51, 4wi 4 . . 3 wff (𝜑 → ¬ 𝜓)
65wn 3 . 2 wff ¬ (𝜑 → ¬ 𝜓)
73, 6wb 196 1 wff ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  pm4.63  384  imnan  386  imp  393  ex  397  dfbi2  460  pm5.32  563  pm4.54  971  nfand  1978  nfanOLD  1981  nfan1  2222  nfan1OLDOLD  2223  nfandOLD  2394  sban  2546  r19.35  3232  dfac5lem4  9152  kmlem3  9179  axrepprim  31916  axunprim  31917  axregprim  31919  axinfprim  31920  axacprim  31921  nolt02o  32181  dfxor4  38584  df3an2  38587  pm11.52  39112
  Copyright terms: Public domain W3C validator