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 387
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 1662) and the constant false (df-fal 1672), we will be able to prove these truth table values: ((⊤ ∧ ⊤) ↔ ⊤) (truantru 1692), ((⊤ ∧ ⊥) ↔ ⊥) (truanfal 1693), ((⊥ ∧ ⊤) ↔ ⊥) (falantru 1694), and ((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1695).

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 253. This is the justification for the definition, along with the fact that it introduces a new symbol . Contrast with (df-or 881), (wi 4), (df-nan 1615), and (df-xor 1640). (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 386 . 2 wff (𝜑𝜓)
42wn 3 . . . 4 wff ¬ 𝜓
51, 4wi 4 . . 3 wff (𝜑 → ¬ 𝜓)
65wn 3 . 2 wff ¬ (𝜑 → ¬ 𝜓)
73, 6wb 198 1 wff ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  pm4.63  388  imnan  390  imp  397  ex  403  dfbi2  468  pm5.32  571  pm4.54  1016  nfand  2002  nfan1  2242  nfan1OLDOLD  2243  sbanv  2340  sban  2530  r19.35  3294  dfac5lem4  9262  kmlem3  9289  axrepprim  32123  axunprim  32124  axregprim  32126  axinfprim  32127  axacprim  32128  nolt02o  32384  dfxor4  38899  df3an2  38902  pm11.52  39426
  Copyright terms: Public domain W3C validator