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 400
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 1541) and the constant false (df-fal 1551), we will be able to prove these truth table values: ((⊤ ∧ ⊤) ↔ ⊤) (truantru 1571), ((⊤ ∧ ⊥) ↔ ⊥) (truanfal 1572), ((⊥ ∧ ⊤) ↔ ⊥) (falantru 1573), and ((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1574).

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 264. This is the justification for the definition, along with the fact that it introduces a new symbol . Contrast with (df-or 845), (wi 4), (df-nan 1483), and (df-xor 1503). (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 399 . 2 wff (𝜑𝜓)
42wn 3 . . . 4 wff ¬ 𝜓
51, 4wi 4 . . 3 wff (𝜑 → ¬ 𝜓)
65wn 3 . 2 wff ¬ (𝜑 → ¬ 𝜓)
73, 6wb 209 1 wff ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  pm4.63  401  imnan  403  imp  410  ex  416  dfbi2  478  pm5.32  577  pm4.54  984  nfand  1899  nfan1  2201  sbanOLD  2313  sbanvOLD  2327  sbanALT  2611  dfac5lem4  9529  kmlem3  9555  axrepprim  32935  axunprim  32936  axregprim  32938  axinfprim  32939  axacprim  32940  nolt02o  33206  dfxor4  40246  df3an2  40249  expandan  40779  ismnuprim  40785  pm11.52  40874
  Copyright terms: Public domain W3C validator