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 T. (df-tru 1319) and the constant false F. (df-fal 1320), we will be able to prove these truth table values: (( T. /\ T. ) <-> T. ) (truantru 1336), (( T. /\ F. ) <-> F. ) (truanfal 1337), (( F. /\ T. ) <-> F. ) (falantru 1338), and (( F. /\ F. ) <-> F. ) (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	|- ((ph /\ ps) <-> -. (ph -> -. ps))

Detailed syntax breakdown of Definition df-an

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3	1, 2	wa 358	. 2 wff (ph /\ ps)
4	2	wn 3	. . . 4 wff -. ps
5	1, 4	wi 4	. . 3 wff (ph -> -. ps)
6	5	wn 3	. 2 wff -. (ph -> -. ps)
7	3, 6	wb 176	1 wff ((ph /\ ps) <-> -. (ph -> -. ps))

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