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 1531) and the constant false (df-fal 1541), we will be able to prove these truth table values: ((⊤ ∧ ⊤) ↔ ⊤) (truantru 1561), ((⊤ ∧ ⊥) ↔ ⊥) (truanfal 1562), ((⊥ ∧ ⊤) ↔ ⊥) (falantru 1563), and ((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1564).

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 262. This is the justification for the definition, along with the fact that it introduces a new symbol . Contrast with (df-or 842), (wi 4), (df-nan 1476), and (df-xor 1496). (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 207 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  980  nfand  1889  nfan1  2191  sbanOLD  2304  sbanvOLD  2318  sbanALT  2606  dfac5lem4  9541  kmlem3  9567  axrepprim  32826  axunprim  32827  axregprim  32829  axinfprim  32830  axacprim  32831  nolt02o  33097  dfxor4  39991  df3an2  39994  expandan  40504  ismnuprim  40510  pm11.52  40599
  Copyright terms: Public domain W3C validator