Definition df-an 241

Description: Define conjunction (logical 'and'). Definition of [Margaris] p. 49.

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 239	. 2 wff (ph /\ ps)
4	2	wn 2	. . . 4 wff -. ps
5	1, 4	wi 3	. . 3 wff (ph -> -. ps)
6	5	wn 2	. 2 wff -. (ph -> -. ps)
7	3, 6	wb 162	1 wff ((ph /\ ps) <-> -. (ph -> -. ps))

This definition is referenced by:  pm4.63 244  iman 254  imnan 259  pm3.2 303  jca 308  anor 326  pm3.26 344  pm3.27 348  impexp 372  anass 485  dfbi2 569  pm5.32 703  pm5.18 719  hban 1194  19.29OLD 1260  19.35 1264  equsex 1351  sban 1445  r19.35 2065  aceq5lem4 5696  kmlem3 5725  nmcopexlem1 11380  nmcfnexlem1 11409  axrepprim 13578  axunprim 13579  axregprim 13581  axinfprim 13582  axacprim 13583  reconnlem1 15128  pm11.52 16024

Copyright terms: Public domain