Definition df-an 360

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 1319) and the constant false ⊥ (df-fal 1320), we will be able to prove these truth table values: (( ⊤ ∧ ⊤ ) ↔ ⊤ ) (truantru 1336), (( ⊤ ∧ ⊥ ) ↔ ⊥ ) (truanfal 1337), (( ⊥ ∧ ⊤ ) ↔ ⊥ ) (falantru 1338), and (( ⊥ ∧ ⊥ ) ↔ ⊥ ) (falanfal 1339).

Contrast with ∨ (df-or 359), → (wi 4), ⊼ (df-nan 1288), and ⊻ (df-xor 1305) . (Contributed by NM, 5-Aug-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 358	. 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 176	1 wff ((φ ∧ ψ) ↔ ¬ (φ → ¬ ψ))

This definition is referenced by:  pm4.63  410  imnan  411  imp  418  ex  423  pm4.54  479  dfbi2  609  pm5.32  617  nfand  1822  nfanOLD  1826  hbanOLD  1829  equsex  1962  sban  2069  r19.35  2759  disj  3592