Definition df-an 225

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 223	. 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 146	1 wff ((ph /\ ps) <-> -. (ph -> -. ps))

This definition is referenced by:  pm4.63 228  iman 237  imnan 242  pm3.2 283  jca 288  anor 304  pm3.26 319  pm3.27 323  impexp 347  anass 439  dfbi2 514  pm5.32 644  hban 1009  19.29 1071  19.35 1075  equsex 1152  sban 1237  r19.35 1759  aceq5lem4 4738  kmlem3 4767  nmcopexlem1 9951  nmcfnexlem1 9980

Copyright terms: Public domain