Definition df-an 435

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

This definition is referenced by:  pm4.63 438  imnan 458  imanOLD 460  imp 489  ex 494  impexpOLD 501  pm3.2OLD 507  anorOLD 518  simplOLD 534  simprOLD 539  jcaOLD 591  anassOLD 730  dfbi2 800  pm5.32 892  pm5.18OLD 1029  hban 1674  19.35 1741  equsex 1822  sban 1912  r19.35 2509  aceq5lem4 6257  kmlem3 6413  nmcopexlem1 12578  nmcfnexlem1 12607  axrepprim 14668  axunprim 14669  axregprim 14671  axinfprim 14672  axacprim 14673  reconnlem1 16531  pm11.52 17427

Copyright terms: Public domain