Definition df-an 386

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 1486) and the constant false ⊥ (df-fal 1489), we will be able to prove these truth table values: ((⊤ ∧ ⊤) ↔ ⊤) (truantru 1506), ((⊤ ∧ ⊥) ↔ ⊥) (truanfal 1507), ((⊥ ∧ ⊤) ↔ ⊥) (falantru 1508), and ((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1509).

Contrast with ∨ (df-or 385), → (wi 4), ⊼ (df-nan 1448), and ⊻ (df-xor 1465) . (Contributed by NM, 5-Jan-1993.)

Assertion

Ref	Expression
df-an	⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))

Detailed syntax breakdown of Definition df-an

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wa 384	. 2 wff (𝜑 ∧ 𝜓)
4	2	wn 3	. . . 4 wff ¬ 𝜓
5	1, 4	wi 4	. . 3 wff (𝜑 → ¬ 𝜓)
6	5	wn 3	. 2 wff ¬ (𝜑 → ¬ 𝜓)
7	3, 6	wb 196	1 wff ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))

This definition is referenced by:  pm4.63  437  imnan  438  imp  445  ex  450  pm4.54  514  dfbi2  660  pm5.32  668  nfand  1826  nfanOLD  1829  nfan1  2068  nfandOLD  2232  sban  2399  r19.35  3084  dfac5lem4  8949  kmlem3  8974  axrepprim  31579  axunprim  31580  axregprim  31582  axinfprim  31583  axacprim  31584  nolt02o  31845  dfxor4  38058  df3an2  38061  pm11.52  38586