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  bi 513  pm5.32 642  hban 985  19.29 1047  19.35 1051  equsex 1135  sban 1221  r19.35 1735  aceq5lem4 4662  kmlem3 4691  nmcopexlem1 10080  nmcfnexlem1 10109

Copyright terms: Public domain